begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem Th11:
:: deftheorem Def1 defines bounded_above SEQ_2:def 1 :
:: deftheorem Def2 defines bounded_below SEQ_2:def 2 :
:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :
:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :
:: deftheorem defines bounded SEQ_2:def 5 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem Th16:
:: deftheorem Def6 defines convergent SEQ_2:def 6 :
:: deftheorem Def7 defines lim SEQ_2:def 7 :
:: deftheorem defines bounded SEQ_2:def 8 :
theorem
canceled;
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem
theorem
theorem Th39:
theorem