reconsider X9 = X as TopStruct ;
let P be Subset of X; :: thesis:
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:
A4: union F = (transl (a,X)) " P

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union F ; :: thesis:
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:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in (transl (a,X)) " P ; :: thesis:
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;
then D in F by A2, A11;
hence x in union F by A13, TARSKI:def 4; :: thesis:

end;

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

end;

end;