let T be TopSpace; :: thesis: for B being Subset-Family of T st B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) holds
B is Basis of T
let B be Subset-Family of T; :: thesis: ( B c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ) implies B is Basis of T )
assume that
A1: B c= the topology of T and
A2: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B & p in a & a c= A ) ; :: thesis: B is Basis of T
thus B c= the topology of T by A1; :: according to CANTOR_1:def 2 :: thesis: the topology of T c= UniCl B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of T or x in UniCl B )
assume A3: x in the topology of T ; :: thesis: x in UniCl B
then reconsider A = x as Subset of T ;
set Y = { V where V is Subset of T : ( V in B & V c= A ) } ;
{ V where V is Subset of T : ( V in B & V c= A ) } c= bool the carrier of T

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { V where V is Subset of T : ( V in B & V c= A ) } or y in bool the carrier of T )
assume y in { V where V is Subset of T : ( V in B & V c= A ) } ; :: thesis: y in bool the carrier of T
then ex V being Subset of T st
( y = V & V in B & V c= A ) ;
hence y in bool the carrier of T ; :: thesis: verum

end;

then reconsider Y = { V where V is Subset of T : ( V in B & V c= A ) } as Subset-Family of T ;
reconsider Y = Y as Subset-Family of T ;
A4: Y c= B

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in B )
assume y in Y ; :: thesis: y in B
then ex V being Subset of T st
( y = V & V in B & V c= A ) ;
hence y in B ; :: thesis: verum

end;

x = union Y

proof

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

let p be set ; :: thesis: ( p in x implies p in union Y )
assume A5: p in x ; :: thesis: p in union Y
then p in A ;
then reconsider q = p as Point of T ;
A is open by A3, PRE_TOPC:def 5;
then consider a being Subset of T such that
A6: ( a in B & q in a & a c= A ) by A2, A5;
a in Y by A6;
hence p in union Y by A6, TARSKI:def 4; :: thesis: verum

end;

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in union Y or p in x )
assume p in union Y ; :: thesis: p in x
then consider a being set such that
A7: ( p in a & a in Y ) by TARSKI:def 4;
ex V being Subset of T st
( a = V & V in B & V c= A ) by A7;
hence p in x by A7; :: thesis: verum

end;

hence x in UniCl B by A4, CANTOR_1:def 1; :: thesis: verum