begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def1 defines bounded_above SEQ_4:def 1 :
:: deftheorem Def2 defines bounded_below SEQ_4:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem SEQ_4:def 3 :
canceled;
:: deftheorem Def4 defines upper_bound SEQ_4:def 4 :
:: deftheorem Def5 defines lower_bound SEQ_4:def 5 :
Lm1:
for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X
Lm2:
for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X
theorem
canceled;
theorem
canceled;
theorem
theorem Th23:
theorem
theorem
theorem Th26:
theorem
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem
theorem
theorem
canceled;
theorem Th35:
theorem
theorem Th37:
theorem
theorem
canceled;
theorem Th40:
theorem
theorem
theorem Th43:
theorem Th44:
theorem
theorem
theorem Th47:
theorem Th48:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th53:
theorem
theorem
theorem Th56:
theorem Th57:
theorem
theorem
begin
theorem Th60:
theorem
theorem Th62:
theorem
theorem
theorem