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: UniCl tE = {{},{}} by YELLOW_9:11;
A2: {{},{}} = tE by ENUMSET1:29;
A3: FinMeetCl tE = {{},{}} by YELLOW_9:11;

A4: now

assume A5: X is empty ; :: thesis:
hence A6: ( 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 A3, A2, A5, A6, YELLOW_9:11; :: thesis:

end;

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

hereby :: thesis:

let o be Subset-Family of X; :: thesis:
set S = TopStruct(# X,o #);
A7: FinMeetCl (union O) c= B by CANTOR_1:1;
assume o in O ; :: thesis:
then A8: 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 A8, XBOOLE_1:1;
then the topology of TopStruct(# X,o #) c= the topology of TT by A7, XBOOLE_1:1;
hence TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) by YELLOW_9:def 5; :: thesis:

end;

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

now

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