begin
set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
set RA = { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;
Lm1:
for x, y being set holds not [x,y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
Lm2:
RAT+ misses { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} }
RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by XBOOLE_1:9;
then Lm3:
REAL+ c= RAT+ \/ { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by XBOOLE_1:1;
REAL+ = RAT+ \/ (( { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+}) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } )
by Lm2, XBOOLE_1:87;
then Lm4:
DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } c= REAL+
by XBOOLE_1:7;
Lm5:
omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;
Lm6:
for s, t being Element of RAT+ st ( for r being Element of RAT+ holds
( r < s iff r < t ) ) holds
s = t
Lm7:
for r being Element of RAT+
for B being set st B in DEDEKIND_CUTS & r in B holds
ex s being Element of RAT+ st
( s in B & r < s )
Lm8:
{} in DEDEKIND_CUTS
Lm9:
DEDEKIND_CUTS /\ RAT+ = {{}}
Lm10:
for x being Element of REAL+ holds
( DEDEKIND_CUT x = {} iff x = {} )
Lm11:
for A being Element of DEDEKIND_CUTS holds
( GLUED A = {} iff A = {} )
Lm12:
for A being Element of DEDEKIND_CUTS holds DEDEKIND_CUT (GLUED A) = A
Lm13:
for x, y being set st x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & not x c= y holds
y c= x
Lm14:
for x9, y9 being Element of RAT+
for x, y being Element of REAL+ st x = x9 & y = y9 holds
( x <=' y iff x9 <=' y9 )
Lm15:
for B being set st B in DEDEKIND_CUTS & B <> {} holds
ex r being Element of RAT+ st
( r in B & r <> {} )
Lm16:
for r, s being Element of RAT+
for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds
s in B
Lm17:
for B being set st B in DEDEKIND_CUTS & B <> {} holds
{} in B
Lm18:
for r being Element of RAT+
for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds
ex s being Element of RAT+ st
( not s in B & s < r )
Lm19:
for x being Element of REAL+ st DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } holds
x in RAT+
Lm20:
for x, y being Element of REAL+ st DEDEKIND_CUT x c= DEDEKIND_CUT y holds
x <=' y
Lm21:
for x, y being Element of REAL+ st x <=' y & y <=' x holds
x = y
Lm22:
for x, y being Element of REAL+ st DEDEKIND_CUT x = DEDEKIND_CUT y holds
x = y
Lm23:
for x being Element of REAL+ holds GLUED (DEDEKIND_CUT x) = x
Lm24:
for B being set st B in DEDEKIND_CUTS holds
ex r being Element of RAT+ st not r in B
Lm25:
for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) c= (A + B) + C
Lm26:
for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) = (A + B) + C
Lm27:
for A, B being Element of DEDEKIND_CUTS holds
( not A + B = {} or A = {} or B = {} )
Lm28:
for e being set st e in REAL+ holds
e <> RAT+
Lm29:
for r, s being Element of RAT+
for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & r in B & s <=' r holds
s in B
Lm30:
for y, x being Element of REAL+ st y < x holds
ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
Lm31:
for x, y, z being Element of REAL+ st x <=' y & y <=' z holds
x <=' z
Lm32:
one = 1
;
Lm33:
{} = {}
;
Lm34:
for A, B being Element of DEDEKIND_CUTS st A + B = A & A <> {} holds
B = {}
Lm35:
for x, y being Element of REAL+ st x + y = x holds
y = {}
Lm36:
for A, B being Element of DEDEKIND_CUTS st A <> {} & A c= B & A <> B holds
ex C being Element of DEDEKIND_CUTS st A + C = B
Lm37:
for x, y being Element of REAL+ st x <=' y holds
DEDEKIND_CUT x c= DEDEKIND_CUT y
Lm38:
for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) c= (A *' B) *' C
Lm39:
for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) = (A *' B) *' C
Lm40:
for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )
Lm41:
for A, B, C being Element of DEDEKIND_CUTS holds A *' (B + C) = (A *' B) + (A *' C)
one in RAT+
;
then reconsider rone = one as Element of REAL+ by Th1;
Lm42:
for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & B <> {} holds
ex r being Element of RAT+ st
( r in B & r <> {} )
Lm43:
for A being Element of DEDEKIND_CUTS st A <> {} holds
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
Lm44:
for A, B being Element of DEDEKIND_CUTS st A = { r where r is Element of RAT+ : r < one } holds
A *' B = B
Lm45:
for i, j being Element of omega
for x9, y9 being Element of RAT+ st i = x9 & j = y9 holds
i +^ j = x9 + y9
Lm46:
for z9, x9, y9 being Element of RAT+ st z9 < x9 + y9 & x9 <> {} & y9 <> {} holds
ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
Lm47:
for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds
ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )