begin
:: deftheorem SUPINF_1:def 1 :
canceled;
:: deftheorem SUPINF_1:def 2 :
canceled;
:: deftheorem SUPINF_1:def 3 :
canceled;
:: deftheorem SUPINF_1:def 4 :
canceled;
:: deftheorem SUPINF_1:def 5 :
canceled;
:: deftheorem SUPINF_1:def 6 :
canceled;
:: deftheorem SUPINF_1:def 7 :
canceled;
:: deftheorem SUPINF_1:def 8 :
canceled;
:: deftheorem SUPINF_1:def 9 :
canceled;
:: deftheorem SUPINF_1:def 10 :
canceled;
:: deftheorem defines bounded_above SUPINF_1:def 11 :
:: deftheorem defines bounded_below SUPINF_1:def 12 :
:: deftheorem SUPINF_1:def 13 :
canceled;
:: deftheorem Def14 defines SetMajorant SUPINF_1:def 14 :
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
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem Def15 defines SetMinorant SUPINF_1:def 15 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem SUPINF_1:def 16 :
canceled;
:: deftheorem SUPINF_1:def 17 :
canceled;
:: deftheorem SUPINF_1:def 18 :
canceled;
:: deftheorem Def19 defines SUP SUPINF_1:def 19 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th112:
theorem Th113:
theorem
:: deftheorem Def20 defines INF SUPINF_1:def 20 :
theorem
canceled;
theorem
canceled;
theorem Th117:
theorem Th118:
theorem