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

proof

now :: thesis:

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:43; :: 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:

now :: 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 A6: a c= o by A4;
TopStruct(# X,o #) is TopSpace by A1, A5;
hence union a in b by A6, PRE_TOPC:def 1; :: thesis:

end;

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

end;

let a, b be Subset of TopStruct(# X,B #); :: thesis:
assume that
A7: a in the topology of TopStruct(# X,B #) and
A8: b in the topology of TopStruct(# X,B #) ; :: thesis:

now :: thesis:

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

end;

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

end;

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

proof

let o be Subset-Family of X; :: thesis:
assume A12: o in O ; :: thesis:
reconsider S = TopStruct(# X,o #) as TopSpace by A1, A12;
Intersect O c= o by A12, MSSUBFAM:2;
then S is TopExtension of TopStruct(# X,B #) by YELLOW_9:def 5;
hence TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ; :: thesis:

end;

reconsider TT = TopStruct(# X,B #) as TopSpace by A2;
let T9 be TopSpace; :: thesis:
assume that
A13: the carrier of T9 = X and
A14: for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T9 ; :: thesis:

now :: thesis:

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

end;

then the topology of T9 c= Intersect O by A13, MSSUBFAM:4;
then TT is TopExtension of T9 by A13, YELLOW_9:def 5;
hence TopStruct(# X,B #) is TopExtension of T9 ; :: thesis: