let X be LinearTopSpace; :: thesis: for E being Subset of X
for x being Point of X st E is open holds
x + E is open
let E be Subset of X; :: thesis: for x being Point of X st E is open holds
x + E is open
let x be Point of X; :: thesis: ( E is open implies x + E is open )
assume A1: E is open ; :: thesis: x + E is open
(transl (x,X)) .: E = x + E by Th33;
hence x + E is open by A1, TOPGRP_1:25; :: thesis: verum