reconsider e = {} (bool {}), tE = {({} {})} as Subset-Family of {} ;
reconsider E = {} (bool (bool {})) as empty Subset-Family of (bool {}) ;
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 dT = TopStruct(# {},tE #) as discrete TopStruct by TDLAT_3:def 1, ZFMISC_1:1;
A1: {{},{}} = tE by ENUMSET1:29;
A2: FinMeetCl tE = {{},{}} by YELLOW_9:11;

A3: now :: thesis:

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

end;

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

hereby :: thesis:

let o be Subset-Family of X; :: thesis:
set S = TopStruct(# X,o #);
A6: FinMeetCl (union O) c= B by CANTOR_1:1;
assume o in O ; :: thesis:
then A7: o c= union O by ZFMISC_1:74;
union O c= FinMeetCl (union O) by CANTOR_1:4;
then o c= FinMeetCl (union O) by A7;
then the topology of TopStruct(# X,o #) c= the topology of TT by A6;
hence TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) by YELLOW_9:def 5; :: thesis:

end;

let T be TopSpace; :: thesis:
assume that
A8: the carrier of T = X and
A9: 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 A8; :: according to YELLOW_9:def 5 :: thesis:
A10: ( X <> {} implies not T is empty ) by A8;

now :: thesis:

let a be set ; :: thesis:
assume A11: a in O ; :: thesis:
then reconsider o = a as Subset-Family of X ;
T is TopExtension of TopStruct(# X,o #) by A9, A11;
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:76;
then FinMeetCl (union O) c= FinMeetCl the topology of T by A8, CANTOR_1:14;
then A12: B c= UniCl (FinMeetCl the topology of T) by A8, CANTOR_1:9;
X in the topology of T by A8, PRE_TOPC:def 1;
hence the topology of TopStruct(# X,B #) c= the topology of T by A12, A10, CANTOR_1:7; :: thesis: