let T be non empty TopStruct ; :: thesis:
let P be Subset-Family of T; :: thesis:
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:
thus P c= the topology of T by A1; :: according to CANTOR_1:def 2 :: thesis:
let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A3: e in the topology of T ; :: thesis:
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 set ; :: according to TARSKI:def 3 :: thesis:
assume e in { V where V is Subset of T : ( V in P & V c= S ) } ; :: thesis:
then ex V being Subset of T st
( e = V & V in P & V c= S ) ;
hence e in P ; :: thesis:

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 set holds
( u in S iff ex Z being set st
( u in Z & Z in X ) )

proof

let u be set ; :: thesis:

hereby :: thesis:

assume A5: u in S ; :: thesis:
then reconsider p = u as Point of T ;
A6: S is open by A3, PRE_TOPC:def 5;
consider B being Basis of p such that
A7: B c= P by A2;
consider W being Subset of T such that
A8: W in B and
A9: W c= S by A5, A6, Def2;
reconsider Z = W as set ;
take Z = Z; :: thesis:
thus u in Z by A8, Th21; :: thesis:
thus Z in X by A7, A8, A9; :: thesis:

end;

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

end;

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