let T be non empty TopSpace; :: thesis:
let P be basis of T; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in the topology of T ; :: thesis:
then reconsider X = x as Subset of T ;
ex Y being Subset-Family of T st
( Y c= Int P & X = union Y )

set Y = { A where A is Subset of T : ( A in Int P & Int A c= X ) } ;
{ A where A is Subset of T : ( A in Int P & Int A c= X ) } c= bool the carrier of T

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { A where A is Subset of T : ( A in Int P & Int A c= X ) } ; :: thesis:
then ex A being Subset of T st
( y = A & A in Int P & Int A c= X ) ;
hence y in bool the carrier of T ; :: thesis:

end;

then reconsider Y = { A where A is Subset of T : ( A in Int P & Int A c= X ) } as Subset-Family of T ;
reconsider Y = Y as Subset-Family of T ;
take Y ; :: thesis:

hereby :: according to TARSKI:def 3 :: thesis:

end;

let y be object ; :: thesis:
assume A2: y in X ; :: thesis:
then reconsider p = y as Point of T ;
reconsider C = P as basis of p by Def4;
X is open by A1;
then p in Int X by A2, TOPS_1:23;
then consider W being Subset of T such that
A3: W in C and
A4: p in Int W and
A5: W c= X by Def1;
Int W c= W by TOPS_1:16;
then A6: Int (Int W) c= X by A5;
Int W in Int P by A3, TDLAT_2:def 1;
then Int W in Y by A6;
hence y in union Y by A4, TARSKI:def 4; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in union Y ; :: thesis:
then consider K being set such that
A7: y in K and
A8: K in Y by TARSKI:def 4;
consider A being Subset of T such that
A9: A = K and
A10: A in Int P and
A11: Int A c= X by A8;
reconsider A = A as Subset of T ;
ex E being Subset of T st
( A = Int E & E in P ) by A10, TDLAT_2:def 1;
hence y in X by A7, A9, A11; :: thesis:

end;