begin
theorem
theorem
canceled;
theorem
theorem Th4:
theorem Th5:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
Lm1:
for M being MetrSpace holds MetrStruct(# the carrier of M,the distance of M #) is MetrSpace
:: deftheorem Def1 defines SubSpace TOPMETR:def 1 :
theorem
canceled;
theorem Th12:
theorem Th13:
:: deftheorem Def2 defines | TOPMETR:def 2 :
:: deftheorem Def3 defines Closed-Interval-MSpace TOPMETR:def 3 :
theorem Th14:
:: deftheorem Def4 defines being_ball-family TOPMETR:def 4 :
theorem Th15:
theorem Th16:
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem
canceled;
theorem Th21:
theorem Th22:
:: deftheorem TOPMETR:def 5 :
canceled;
:: deftheorem Def6 defines compact TOPMETR:def 6 :
theorem
:: deftheorem defines R^1 TOPMETR:def 7 :
theorem Th24:
:: deftheorem defines Closed-Interval-TSpace TOPMETR:def 8 :
theorem Th25:
theorem Th26:
theorem Th27:
Lm2:
for a, b, r being real number st r >= 0 & a + r <= b holds
a <= b
theorem
theorem
theorem Th30:
theorem