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

proof

let P be Subset of X; :: 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 X 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:19; :: thesis: verum