let T be non empty TopStruct ; :: thesis: for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds
P is Basis of T
let P be Subset-Family of T; :: thesis: ( P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) implies P is Basis of T )
assume that
A1: P c= the topology of T and
A2: for x being Point of T ex B being Basis of x st B c= P ; :: thesis: P is Basis of T
P is quasi_basis

proof

let e be object ; :: according to TARSKI:def 3,CANTOR_1:def 2 :: thesis: ( not e in the topology of T or e in UniCl P )
assume A3: e in the topology of T ; :: thesis: e in UniCl P
then reconsider S = e as Subset of T ;
set X = { V where V is Subset of T : ( V in P & V c= S ) } ;
A4: { V where V is Subset of T : ( V in P & V c= S ) } c= P

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { V where V is Subset of T : ( V in P & V c= S ) } or e in P )
assume e in { V where V is Subset of T : ( V in P & V c= S ) } ; :: thesis: e in P
then ex V being Subset of T st
( e = V & V in P & V c= S ) ;
hence e in P ; :: thesis: verum

end;

then reconsider X = { V where V is Subset of T : ( V in P & V c= S ) } as Subset-Family of T by XBOOLE_1:1;
for u being object holds
( u in S iff ex Z being set st
( u in Z & Z in X ) )

proof

let u be object ; :: thesis: ( u in S iff ex Z being set st
( u in Z & Z in X ) )

hereby :: thesis: ( ex Z being set st
( u in Z & Z in X ) implies u in S )

assume A5: u in S ; :: thesis: ex Z being set st
( u in Z & Z in X )
then reconsider p = u as Point of T ;
consider B being Basis of p such that
A6: B c= P by A2;
S is open by A3;
then consider W being Subset of T such that
A7: W in B and
A8: W c= S by A5, Def1;
reconsider Z = W as set ;
take Z = Z; :: thesis: ( u in Z & Z in X )
thus u in Z by A7, Th12; :: thesis: Z in X
thus Z in X by A6, A7, A8; :: thesis: verum

end;

given Z being set such that A9: u in Z and
A10: Z in X ; :: thesis: u in S
ex V being Subset of T st
( V = Z & V in P & V c= S ) by A10;
hence u in S by A9; :: thesis: verum

end;

then S = union X by TARSKI:def 4;
hence e in UniCl P by A4, CANTOR_1:def 1; :: thesis: verum

end;

hence P is Basis of T by A1, TOPS_2:64; :: thesis: verum