let PM be MetrStruct ; TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
set T = TopStruct(# the carrier of PM,(Family_open_set PM) #);
A1:
for p, q being Subset of TopStruct(# the carrier of PM,(Family_open_set PM) #) st p in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) & q in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) holds
p /\ q in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #)
by Th31;
( the carrier of TopStruct(# the carrier of PM,(Family_open_set PM) #) in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) & ( for a being Subset-Family of TopStruct(# the carrier of PM,(Family_open_set PM) #) st a c= the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) holds
union a in the topology of TopStruct(# the carrier of PM,(Family_open_set PM) #) ) )
by Th30, Th32;
hence
TopStruct(# the carrier of PM,(Family_open_set PM) #) is TopSpace
by A1, PRE_TOPC:def 1; verum