let X be LinearTopSpace; :: thesis: for E being open Subset of
for K being Subset of holds K + E is open
let E be open Subset of ; :: thesis: for K being Subset of holds K + E is open
let K be Subset of ; :: thesis: K + E is open
reconsider F = { (a + E) where a is Point of : a in K } as Subset-Family of by Lm2;
A1: F is open

proof

let P be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
then ex a being Point of st
( P = a + E & a in K ) ;
hence P is open ; :: thesis: verum

end;

K + E = union F by Th4;
hence K + E is open by A1, TOPS_2:26; :: thesis: verum