begin
theorem Th1:
theorem Th2:
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
set M0 = MetrStruct(# 1,Empty^2-to-zero #);
:: deftheorem Def1 defines Discerning SUB_METR:def 1 :
:: deftheorem Def2 defines Discerning SUB_METR:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th14:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
:: deftheorem SUB_METR:def 3 :
canceled;
:: deftheorem Def4 defines ultra SUB_METR:def 4 :
definition
func Set_to_zero -> Function of
[:{{} ,{{} }},{{} ,{{} }}:],
REAL equals
[:{{} ,{{} }},{{} ,{{} }}:] --> 0 ;
coherence
[:{{} ,{{} }},{{} ,{{} }}:] --> 0 is Function of [:{{} ,{{} }},{{} ,{{} }}:],REAL
;
end;
:: deftheorem defines Set_to_zero SUB_METR:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th40:
theorem
canceled;
theorem Th42:
theorem Th43:
:: deftheorem defines ZeroSpace SUB_METR:def 6 :
:: deftheorem Def7 defines is_between SUB_METR:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
:: deftheorem defines open_dist_Segment SUB_METR:def 8 :
theorem
canceled;
theorem
:: deftheorem defines close_dist_Segment SUB_METR:def 9 :
theorem
canceled;
theorem