let X be set ; :: thesis:
let O be Subset-Family of (bool X); :: thesis:
reconsider B = UniCl (FinMeetCl (union O)) as Subset-Family of X ;
take B ; :: thesis:
thus B = UniCl (FinMeetCl (union O)) ; :: thesis:
reconsider E = {} (bool (bool {} )) as empty Subset-Family of (bool {} ) ;
reconsider e = {} (bool {} ), tE = {({} {} )} as Subset-Family of {} ;
reconsider dT = TopStruct(# {} ,tE #) as discrete TopStruct by TDLAT_3:def 1, ZFMISC_1:1;
A1: ( UniCl tE = {{} ,{} } & FinMeetCl e = tE ) by YELLOW_9:11, YELLOW_9:17;
A2: ( FinMeetCl tE = {{} ,{} } & {{} ,{} } = tE ) by ENUMSET1:69, YELLOW_9:11;

A3: now

assume A4: X is empty ; :: thesis:
hence A5: ( union O = e or union O = tE ) by ZFMISC_1:1, ZFMISC_1:39; :: thesis:
thus FinMeetCl (union E) = the topology of dT by YELLOW_9:17; :: thesis:
hence TopStruct(# X,B #) is TopSpace by A2, A4, A5, YELLOW_9:11; :: thesis:

end;

hence TopStruct(# X,B #) is TopSpace by CANTOR_1:17; :: thesis:
reconsider TT = TopStruct(# X,B #) as TopSpace by A3, CANTOR_1:17;

hereby :: thesis:

let o be Subset-Family of X; :: thesis:
set S = TopStruct(# X,o #);
assume A6: o in O ; :: thesis:
TT is TopExtension of TopStruct(# X,o #)

thus the carrier of TopStruct(# X,o #) = the carrier of TT ; :: according to YELLOW_9:def 5 :: thesis:
( o c= union O & union O c= FinMeetCl (union O) ) by A6, CANTOR_1:4, ZFMISC_1:92;
then ( o c= FinMeetCl (union O) & FinMeetCl (union O) c= B ) by CANTOR_1:1, XBOOLE_1:1;
hence the topology of TopStruct(# X,o #) c= the topology of TT by XBOOLE_1:1; :: thesis:

end;

hence TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ; :: thesis:

end;

let T be TopSpace; :: thesis:
assume that
A7: the carrier of T = X and
A8: for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ; :: thesis:
thus the carrier of T = the carrier of TopStruct(# X,B #) by A7; :: according to YELLOW_9:def 5 :: thesis:
A9: X in the topology of T by A7, PRE_TOPC:def 1;

let a be set ; :: thesis:
assume A10: a in O ; :: thesis:
then reconsider o = a as Subset-Family of X ;
T is TopExtension of TopStruct(# X,o #) by A8, A10;
hence a c= the topology of T by YELLOW_9:def 5; :: thesis:

end;

then union O c= the topology of T by ZFMISC_1:94;
then FinMeetCl (union O) c= FinMeetCl the topology of T by A7, CANTOR_1:16;
then A11: B c= UniCl (FinMeetCl the topology of T) by A7, CANTOR_1:9;
( X <> {} implies not T is empty ) by A7;
hence the topology of TopStruct(# X,B #) c= the topology of T by A1, A2, A3, A9, A11, CANTOR_1:7, ZFMISC_1:37; :: thesis: