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

proof

let x be object ; :: according to TARSKI:def 3,CANTOR_1:def 2 :: thesis: ( not x in the topology of T or x in UniCl B )
assume A4: 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 object ; :: 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 ;
A5: Y c= B

proof

let y be object ; :: 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;

A = union Y

proof

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

let p be object ; :: thesis: ( p in A implies p in union Y )
assume A6: p in A ; :: thesis: p in union Y
then p in A ;
then reconsider q = p as Point of T ;
A is open by A4;
then consider a being Subset of T such that
A7: a in B and
A8: q in a and
A9: a c= A by A2, A6;
a in Y by A7, A9;
hence p in union Y by A8, TARSKI:def 4; :: thesis: verum

end;

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

end;

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

end;

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