let X be LinearTopSpace; :: thesis: for V1, V2, V being Subset of X st V1 + V2 c= V holds
(Int V1) + (Int V2) c= Int V
let V1, V2, V be Subset of X; :: thesis: ( V1 + V2 c= V implies (Int V1) + (Int V2) c= Int V )
assume A1: V1 + V2 c= V ; :: thesis: (Int V1) + (Int V2) c= Int V
( Int V1 c= V1 & Int V2 c= V2 ) by TOPS_1:16;
then (Int V1) + (Int V2) c= V1 + V2 by Th11;
then (Int V1) + (Int V2) c= V by A1;
hence (Int V1) + (Int V2) c= Int V by TOPS_1:24; :: thesis: verum