theorem :: PCOMPS_2:5

for PT being non empty TopSpace
for PM being MetrSpace
for FX being Subset-Family of PT
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
( FX is Subset-Family of PT iff FX is Subset-Family of PM ) by Th4;