let a, b be Element of REAL ; :: thesis: not (0,one) --> (a,b) in REAL

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 f = (0,one) --> (a,b);

for x, y being set holds not {[0,x],[one,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 ) ) }

then not (0,one) --> (a,b) in REAL+ by A26, ARYTM_2:def 2, XBOOLE_0:def 3;

hence not (0,one) --> (a,b) in REAL by A1, XBOOLE_0:def 3; :: thesis: verum

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 f = (0,one) --> (a,b);

A1: now :: thesis: not (0,one) --> (a,b) in [:{{}},REAL+:]

A6:
(0,one) --> (a,b) = {[0,a],[one,b]}
by FUNCT_4:67;
(0,one) --> (a,b) = {[0,a],[one,b]}
by FUNCT_4:67;

then A2: [one,b] in (0,one) --> (a,b) by TARSKI:def 2;

assume (0,one) --> (a,b) in [:{{}},REAL+:] ; :: thesis: contradiction

then consider x, y being object such that

A3: x in {{}} and

y in REAL+ and

A4: (0,one) --> (a,b) = [x,y] by ZFMISC_1:84;

A5: x = 0 by A3, TARSKI:def 1;

end;then A2: [one,b] in (0,one) --> (a,b) by TARSKI:def 2;

assume (0,one) --> (a,b) in [:{{}},REAL+:] ; :: thesis: contradiction

then consider x, y being object such that

A3: x in {{}} and

y in REAL+ and

A4: (0,one) --> (a,b) = [x,y] by ZFMISC_1:84;

A5: x = 0 by A3, TARSKI:def 1;

now :: thesis: not (0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) }

then A18:
not (0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) } \ { [k,one] where k is Element of NAT : verum }
;assume
(0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) }
; :: thesis: contradiction

then consider i, j being Element of NAT such that

A7: (0,one) --> (a,b) = [i,j] and

i,j are_coprime and

j <> {} ;

A8: ( {i} in (0,one) --> (a,b) & {i,j} in (0,one) --> (a,b) ) by A7, TARSKI:def 2;

end;then consider i, j being Element of NAT such that

A7: (0,one) --> (a,b) = [i,j] and

i,j are_coprime and

j <> {} ;

A8: ( {i} in (0,one) --> (a,b) & {i,j} in (0,one) --> (a,b) ) by A7, TARSKI:def 2;

A9: now :: thesis: not i = j

assume
i = j
; :: thesis: contradiction

then {i} = {i,j} by ENUMSET1:29;

then A10: [i,j] = {{i}} by ENUMSET1:29;

then [one,b] in {{i}} by A6, A7, TARSKI:def 2;

then A11: [one,b] = {i} by TARSKI:def 1;

[0,a] in {{i}} by A6, A7, A10, TARSKI:def 2;

then [0,a] = {i} by TARSKI:def 1;

hence contradiction by A11, XTUPLE_0:1; :: thesis: verum

end;then {i} = {i,j} by ENUMSET1:29;

then A10: [i,j] = {{i}} by ENUMSET1:29;

then [one,b] in {{i}} by A6, A7, TARSKI:def 2;

then A11: [one,b] = {i} by TARSKI:def 1;

[0,a] in {{i}} by A6, A7, A10, TARSKI:def 2;

then [0,a] = {i} by TARSKI:def 1;

hence contradiction by A11, XTUPLE_0:1; :: thesis: verum

per cases
( ( {i,j} = [0,a] & {i} = [0,a] ) or ( {i,j} = [0,a] & {i} = [one,b] ) or ( {i,j} = [one,b] & {i} = [0,a] ) or ( {i,j} = [one,b] & {i} = [one,b] ) )
by A6, A8, TARSKI:def 2;

end;

suppose that A12:
{i,j} = [0,a]
and

A13: {i} = [one,b] ; :: thesis: contradiction

A13: {i} = [one,b] ; :: thesis: contradiction

i in {{0},{0,a}}
by A12, TARSKI:def 2;

then ( i = {0,a} or i = {0} ) by TARSKI:def 2;

then A14: 0 in i by TARSKI:def 1, TARSKI:def 2;

i = {one} by A13, Lm6;

hence contradiction by A14, TARSKI:def 1; :: thesis: verum

end;then ( i = {0,a} or i = {0} ) by TARSKI:def 2;

then A14: 0 in i by TARSKI:def 1, TARSKI:def 2;

i = {one} by A13, Lm6;

hence contradiction by A14, TARSKI:def 1; :: thesis: verum

suppose that A15:
{i,j} = [one,b]
and

A16: {i} = [0,a] ; :: thesis: contradiction

A16: {i} = [0,a] ; :: thesis: contradiction

i in {{one},{one,b}}
by A15, TARSKI:def 2;

then ( i = {one,b} or i = {one} ) by TARSKI:def 2;

then A17: one in i by TARSKI:def 1, TARSKI:def 2;

i = {0} by A16, Lm6;

hence contradiction by A17, TARSKI:def 1; :: thesis: verum

end;then ( i = {one,b} or i = {one} ) by TARSKI:def 2;

then A17: one in i by TARSKI:def 1, TARSKI:def 2;

i = {0} by A16, Lm6;

hence contradiction by A17, TARSKI:def 1; :: thesis: verum

for x, y being set holds not {[0,x],[one,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 ) ) }

proof

then A26:
not (0,one) --> (a,b) in DEDEKIND_CUTS
by A6, ARYTM_2:def 1;
given x, y being set such that A19:
{[0,x],[one,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 ) ) } ; :: thesis: contradiction

consider A being Subset of RAT+ such that

A20: {[0,x],[one,y]} = A and

A21: 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 A19;

( [0,x] in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds

s in A ) ) by A20, A21, TARSKI:def 2;

then consider r1, r2, r3 being Element of RAT+ such that

A22: r1 in A and

A23: r2 in A and

A24: ( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) by ARYTM_3:75;

A25: ( r2 = [0,x] or r2 = [one,y] ) by A20, A23, TARSKI:def 2;

( r1 = [0,x] or r1 = [one,y] ) by A20, A22, TARSKI:def 2;

hence contradiction by A20, A24, A25, TARSKI:def 2; :: thesis: verum

end;( ( 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 ) ) } ; :: thesis: contradiction

consider A being Subset of RAT+ such that

A20: {[0,x],[one,y]} = A and

A21: 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 A19;

( [0,x] in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds

s in A ) ) by A20, A21, TARSKI:def 2;

then consider r1, r2, r3 being Element of RAT+ such that

A22: r1 in A and

A23: r2 in A and

A24: ( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) by ARYTM_3:75;

A25: ( r2 = [0,x] or r2 = [one,y] ) by A20, A23, TARSKI:def 2;

( r1 = [0,x] or r1 = [one,y] ) by A20, A22, TARSKI:def 2;

hence contradiction by A20, A24, A25, TARSKI:def 2; :: thesis: verum

now :: thesis: not (0,one) --> (a,b) in omega

then
not (0,one) --> (a,b) in RAT+
by A18, XBOOLE_0:def 3;assume
(0,one) --> (a,b) in omega
; :: thesis: contradiction

then {} in (0,one) --> (a,b) by ORDINAL3:8;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

end;then {} in (0,one) --> (a,b) by ORDINAL3:8;

hence contradiction by A6, TARSKI:def 2; :: thesis: verum

then not (0,one) --> (a,b) in REAL+ by A26, ARYTM_2:def 2, XBOOLE_0:def 3;

hence not (0,one) --> (a,b) in REAL by A1, XBOOLE_0:def 3; :: thesis: verum