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

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

hence
P is Basis of T
by A1, TOPS_2:64; :: thesis: verum
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

for u being object holds

( u in S iff ex Z being set st

( u in Z & Z in X ) )

hence e in UniCl P by A4, CANTOR_1:def 1; :: thesis: verum

end;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

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;
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;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

for u being object holds

( u in S iff ex Z being set st

( u in Z & Z in X ) )

proof

then
S = union X
by TARSKI:def 4;
let u be object ; :: thesis: ( u in S iff ex Z being set st

( u in Z & Z in X ) )

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;( u in Z & Z in X ) )

hereby :: thesis: ( ex Z being set st

( u in Z & Z in X ) implies u in S )

given Z being set such that A9:
u in Z
and ( 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;( 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

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

hence e in UniCl P by A4, CANTOR_1:def 1; :: thesis: verum