let X be set ; :: thesis:
let O be Subset-Family of (bool X); :: thesis:
assume A1: for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ; :: thesis:
reconsider B = Intersect O as Subset-Family of X ;
set T = TopStruct(# X,B #);
take B ; :: thesis:
thus B = Intersect O ; :: thesis:
A2: TopStruct(# X,B #) is TopSpace-like

thus the carrier of TopStruct(# X,B #) in bool the carrier of TopStruct(# X,B #) by ZFMISC_1:def 1; :: thesis:
let a be set ; :: thesis:
assume A3: a in O ; :: thesis:
then reconsider o = a as Subset-Family of X ;
TopStruct(# X,o #) is TopSpace by A1, A3;
hence the carrier of TopStruct(# X,B #) in a by PRE_TOPC:def 1; :: thesis:

end;

hence the carrier of TopStruct(# X,B #) in the topology of TopStruct(# X,B #) by SETFAM_1:58; :: according to PRE_TOPC:def 1 :: thesis:

hereby :: thesis:

let a be Subset-Family of TopStruct(# X,B #); :: thesis:
assume A4: a c= the topology of TopStruct(# X,B #) ; :: thesis:

let b be set ; :: thesis:
assume A5: b in O ; :: thesis:
then reconsider o = b as Subset-Family of X ;
B c= b by A5, MSSUBFAM:2;
then ( a c= o & TopStruct(# X,o #) is TopSpace ) by A1, A4, A5, XBOOLE_1:1;
hence union a in b by PRE_TOPC:def 1; :: thesis:

end;

hence union a in the topology of TopStruct(# X,B #) by SETFAM_1:58; :: thesis:

end;

let a, b be Subset of TopStruct(# X,B #); :: thesis:
assume A6: ( a in the topology of TopStruct(# X,B #) & b in the topology of TopStruct(# X,B #) ) ; :: thesis:

let c be set ; :: thesis:
assume A7: c in O ; :: thesis:
then reconsider o = c as Subset-Family of X ;
( a in o & b in o & TopStruct(# X,o #) is TopSpace ) by A1, A6, A7, SETFAM_1:58;
hence a /\ b in c by PRE_TOPC:def 1; :: thesis:

end;

hence a /\ b in the topology of TopStruct(# X,B #) by SETFAM_1:58; :: thesis:

end;

hence TopStruct(# X,B #) is TopSpace ; :: thesis:
reconsider TT = TopStruct(# X,B #) as TopSpace by A2;
thus for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) :: thesis:

let o be Subset-Family of X; :: thesis:
assume A8: o in O ; :: thesis:
reconsider S = TopStruct(# X,o #) as TopSpace by A1, A8;
S is TopExtension of TopStruct(# X,B #)

thus the carrier of TopStruct(# X,B #) = the carrier of S ; :: according to YELLOW_9:def 5 :: thesis:
thus the topology of TopStruct(# X,B #) c= the topology of S by A8, MSSUBFAM:2; :: thesis:

end;

hence TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ; :: 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
TopStruct(# X,o #) is TopExtension of T' ; :: thesis:
TT is TopExtension of T'

thus the carrier of T' = the carrier of TT by A9; :: according to YELLOW_9:def 5 :: thesis:

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

end;

hence the topology of T' c= the topology of TT by A9, MSSUBFAM:4; :: thesis:

end;

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