:: deftheorem defines Closed-Interval-TSpace TOPMETR:def 7 :
for a, b being Real holds Closed-Interval-TSpace (a,b) = TopSpaceMetr (Closed-Interval-MSpace (a,b));