let X be LinearTopSpace; :: thesis: for A, B being Subset of X holds (Int A) + (Int B) c= Int (A + B)
let A, B be Subset of X; :: thesis: (Int A) + (Int B) c= Int (A + B)
( Int A c= A & Int B c= B ) by TOPS_1:16;
then (Int A) + (Int B) c= A + B by Th11;
hence (Int A) + (Int B) c= Int (A + B) by TOPS_1:24; :: thesis: verum