let V be RealUnitarySpace; :: thesis: TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace
set T = TopStruct(# the carrier of V,(Family_open_set V) #);
A1: the carrier of TopStruct(# the carrier of V,(Family_open_set V) #) in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) by Th38;
A2: for a being Subset-Family of TopStruct(# the carrier of V,(Family_open_set V) #) st a c= the topology of TopStruct(# the carrier of V,(Family_open_set V) #) holds
union a in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) by Th40;
for p, q being Subset of TopStruct(# the carrier of V,(Family_open_set V) #) st p in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) & q in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) holds
p /\ q in the topology of TopStruct(# the carrier of V,(Family_open_set V) #) by Th39;
hence TopStruct(# the carrier of V,(Family_open_set V) #) is TopSpace by A1, A2, PRE_TOPC:def 1; :: thesis: verum