let X be LinearTopSpace; :: thesis: for D being closed Subset of X
for x being Point of X holds x + D is closed
let D be closed Subset of X; :: thesis: for x being Point of X holds x + D is closed
let x be Point of X; :: thesis: x + D is closed
(transl (x,X)) .: D = x + D by Th33;
hence x + D is closed by TOPS_2:58; :: thesis: verum