begin
:: deftheorem Def1 defines UpperBound XXREAL_2:def 1 :
:: deftheorem Def2 defines LowerBound XXREAL_2:def 2 :
:: deftheorem Def3 defines sup XXREAL_2:def 3 :
:: deftheorem Def4 defines inf XXREAL_2:def 4 :
:: deftheorem Def5 defines left_end XXREAL_2:def 5 :
:: deftheorem Def6 defines right_end XXREAL_2:def 6 :
theorem Th1:
theorem Th2:
Lm1:
for x being ext-real number holds sup {x} = x
Lm2:
for x being ext-real number holds inf {x} = x
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def7 defines inf XXREAL_2:def 7 :
:: deftheorem Def8 defines sup XXREAL_2:def 8 :
theorem
Lm3:
for x, y being ext-real number st x <= y holds
y is UpperBound of {x,y}
Lm4:
for x, y being ext-real number
for z being UpperBound of {x,y} holds y <= z
theorem
theorem
Lm5:
for y, x being ext-real number st y <= x holds
y is LowerBound of {x,y}
Lm6:
for x, y being ext-real number
for z being LowerBound of {x,y} holds z <= y
theorem
:: deftheorem Def9 defines bounded_below XXREAL_2:def 9 :
:: deftheorem Def10 defines bounded_above XXREAL_2:def 10 :
:: deftheorem Def11 defines bounded XXREAL_2:def 11 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem
theorem
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem
theorem
theorem
theorem Th65:
theorem Th66:
theorem
theorem
theorem Th69:
theorem Th70:
theorem
theorem
theorem Th73:
theorem
theorem Th75:
theorem Th76:
theorem
theorem
begin
:: deftheorem Def12 defines connected XXREAL_2:def 12 :
theorem
theorem
theorem
theorem Th82:
theorem
theorem Th84:
theorem Th85:
theorem Th86:
theorem
theorem Th88:
theorem
theorem
theorem
theorem Th92:
theorem
theorem
theorem