let T be TopSpace; :: thesis:
let B be Subset-Family of T; :: thesis:
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:
A3: B is open by A1, TOPS_2:64;
B is quasi_basis

let x be object ; :: according to TARSKI:def 3,CANTOR_1:def 2 :: thesis:
assume A4: x in the topology of T ; :: thesis:
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

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { V where V is Subset of T : ( V in B & V c= A ) } ; :: thesis:
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:

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

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

end;

let p be object ; :: thesis:
assume A6: p in A ; :: thesis:
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:

end;

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in union Y ; :: thesis:
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:

end;

end;