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

proof

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { A where A is Subset of T : ( A in Int P & Int A c= X ) } or y in bool the carrier of T )
assume y in { A where A is Subset of T : ( A in Int P & Int A c= X ) } ; :: thesis: y in bool the carrier of T
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: verum

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: ( Y c= Int P & X = union Y )

hereby :: according to TARSKI:def 3 :: thesis: X = union Y

let y be object ; :: thesis: ( y in Y implies y in Int P )
assume y in Y ; :: thesis: y in Int P
then ex A being Subset of T st
( y = A & A in Int P & Int A c= X ) ;
hence y in Int P ; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union Y c= X

let y be object ; :: thesis: ( y in X implies y in union Y )
assume A2: y in X ; :: thesis: y in union Y
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: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in union Y or y in X )
assume y in union Y ; :: thesis: y in X
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: verum

end;

hence x in UniCl (Int P) by CANTOR_1:def 1; :: thesis: verum