set T = TopStruct(# the carrier of ET,(Family_open_set ET) #);
A1: for a being Subset-Family of TopStruct(# the carrier of ET,(Family_open_set ET) #) st a c= the topology of TopStruct(# the carrier of ET,(Family_open_set ET) #) holds
union a in the topology of TopStruct(# the carrier of ET,(Family_open_set ET) #) by Th9;
for a, b being Subset of ET st a in the topology of TopStruct(# the carrier of ET,(Family_open_set ET) #) & b in the topology of TopStruct(# the carrier of ET,(Family_open_set ET) #) holds
a /\ b in Family_open_set ET by Th9;
then TopStruct(# the carrier of ET,(Family_open_set ET) #) is TopSpace by A1, Th9, PRE_TOPC:def 1;
hence ex b₁ being strict TopSpace st
( the carrier of b₁ = the carrier of ET & Family_open_set ET = the topology of b₁ ) ; :: thesis: verum