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
A11: B is open by A1, TOPS_2:78;
B is quasi_basis

proof

let x be set ; :: according to TARSKI:def 3,CANTOR_1:def 2 :: 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 ;
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 and
A7: q in a and
A8: a c= A by A2, A5;
a in Y by A6, A8;
hence p in union Y by A7, 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
A9: p in a and
A10: a in Y by TARSKI:def 4;
ex V being Subset of T st
( a = V & V in B & V c= A ) by A10;
hence p in x by A9; :: thesis: verum

end;

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

end;

hence B is Basis of T by A11; :: thesis: verum