let X be LinearTopSpace; :: thesis: for a being Point of X holds transl a,X is continuous
let a be Point of X; :: thesis: transl a,X is continuous
A1: [#] X <> {} ;

now

let P be Subset of X; :: thesis: ( P is open implies (transl a,X) " P is open )
assume A2: P is open ; :: thesis: (transl a,X) " P is open
reconsider X' = X as TopStruct ;
defpred S₁[ Subset of X'] means ex D being Subset of X st
( D = $1 & D is open & a + D c= P );
consider F being Subset-Family of X' such that
A3: for A being Subset of X' holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
reconsider F = F as Subset-Family of X ;
A4: F is open

proof

let A be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( not A in F or A is open )
assume A in F ; :: thesis: A is open
then ex D being Subset of X st
( D = A & D is open & a + D c= P ) by A3;
hence A is open ; :: thesis: verum

end;

union F = (transl a,X) " P

proof

thus union F c= (transl a,X) " P :: according to XBOOLE_0:def 10 :: thesis: (transl a,X) " P c= union F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in (transl a,X) " P )
assume x in union F ; :: thesis: x in (transl a,X) " P
then consider A being set such that
A5: x in A and
A6: A in F by TARSKI:def 4;
consider D being Subset of X such that
A7: D = A and
D is open and
A8: a + D c= P by A3, A6;
reconsider x = x as Point of X by A5, A6;
a + D = { (a + u) where u is Point of X : u in D } by RUSUB_4:def 9;
then A9: a + x in a + D by A5, A7;
(transl a,X) . x = a + x by Def10;
hence x in (transl a,X) " P by A8, A9, FUNCT_2:46; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (transl a,X) " P or x in union F )
assume A10: x in (transl a,X) " P ; :: thesis: x in union F
then reconsider x = x as Point of X ;
(transl a,X) . x in P by A10, FUNCT_2:46;
then a + x in P by Def10;
then consider V, D being Subset of X such that
V is open and
A11: D is open and
A12: a in V and
A13: x in D and
A14: V + D c= P by A2, Def8;
A15: {a} + D = a + D by RUSUB_4:36;
{a} c= V by A12, ZFMISC_1:37;
then a + D c= V + D by A15, Th10;
then a + D c= P by A14, XBOOLE_1:1;
then D in F by A3, A11;
hence x in union F by A13, TARSKI:def 4; :: thesis: verum

end;

hence (transl a,X) " P is open by A4, TOPS_2:26; :: thesis: verum

end;

hence transl a,X is continuous by A1, TOPS_2:55; :: thesis: verum