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: now

reconsider X9 = X as TopStruct ;
let P be Subset of X; :: thesis: ( P is open implies (transl (a,X)) " P is open )
defpred S₁[ Subset of X9] means ex D being Subset of X st
( D = $1 & D is open & a + D c= P );
consider F being Subset-Family of X9 such that
A2: for A being Subset of X9 holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
reconsider F = F as Subset-Family of X ;
assume A3: P is open ; :: thesis: (transl (a,X)) " P is open
A4: 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;
reconsider x = x as Point of X by A5, A6;
A7: (transl (a,X)) . x = a + x by Def10;
consider D being Subset of X such that
A8: D = A and
D is open and
A9: a + D c= P by A2, A6;
a + D = { (a + u) where u is Point of X : u in D } by RUSUB_4:def 8;
then a + x in a + D by A5, A8;
hence x in (transl (a,X)) " P by A9, A7, FUNCT_2:38; :: 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:38;
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 A3, Def8;
( {a} + D = a + D & {a} c= V ) by A12, RUSUB_4:33, ZFMISC_1:31;
then a + D c= V + D by Th10;
then a + D c= P by A14, XBOOLE_1:1;
then D in F by A2, A11;
hence x in union F by A13, TARSKI:def 4; :: thesis: verum

end;

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 A2;
hence A is open ; :: thesis: verum

end;

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

end;

[#] X <> {} ;
hence transl (a,X) is continuous by A1, TOPS_2:43; :: thesis: verum