:: deftheorem defines metrizable PCOMPS_1:def 8 :
for IT being TopStruct holds
( IT is metrizable iff ex f being Function of [: the carrier of IT, the carrier of IT:],REAL st
( f is_metric_of the carrier of IT & Family_open_set (SpaceMetr ( the carrier of IT,f)) = the topology of IT ) );