:: deftheorem defines compact TOPMETR:def 5 :
for M being MetrStruct holds
( M is compact iff TopSpaceMetr M is compact );