begin
:: deftheorem Def1 defines is_way_below WAYBEL_3:def 1 :
:: deftheorem Def2 defines compact WAYBEL_3:def 2 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
:: deftheorem defines waybelow WAYBEL_3:def 3 :
:: deftheorem defines wayabove WAYBEL_3:def 4 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
theorem Th16:
theorem
begin
theorem Th18:
theorem
theorem
theorem Th21:
theorem
theorem
begin
:: deftheorem Def5 defines satisfying_axiom_of_approximation WAYBEL_3:def 5 :
:: deftheorem Def6 defines continuous WAYBEL_3:def 6 :
theorem
theorem
theorem
begin
:: deftheorem Def7 defines non-Empty WAYBEL_3:def 7 :
:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def 8 :
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
begin
theorem Th34:
theorem Th35:
theorem Th36:
theorem
:: deftheorem Def9 defines locally-compact WAYBEL_3:def 9 :
theorem
canceled;
theorem Th39:
theorem Th40:
theorem
theorem
theorem