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);

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

(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;

per cases ( {{one,b},{one}} = {0} or {{one,b},{one}} = {0,y} ) by A4, A5, A2, TARSKI:def 2;

suppose {{one,b},{one}} = {0} ; :: thesis: contradiction

then 0 in {{one,b},{one}} by TARSKI:def 1;
hence contradiction by TARSKI:def 2; :: thesis: verum

end;

suppose {{one,b},{one}} = {0,y} ; :: thesis: contradiction

then 0 in {{one,b},{one}} by TARSKI:def 2;
hence contradiction by TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

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

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;

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;

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;

suppose ( {i,j} = [0,a] & {i} = [0,a] ) ; :: thesis: contradiction

hence contradiction by A9, ZFMISC_1:5; :: thesis: verum

end;

suppose that A12: {i,j} = [0,a] and
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;

suppose that A15: {i,j} = [one,b] and
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;

suppose ( {i,j} = [one,b] & {i} = [one,b] ) ; :: thesis: contradiction

hence contradiction by A9, ZFMISC_1:5; :: thesis: verum

end;

end;

end;

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 } ;
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

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;

then A26: not (0,one) --> (a,b) in DEDEKIND_CUTS by A6, ARYTM_2:def 1;

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

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 not (0,one) --> (a,b) in RAT+ by A18, XBOOLE_0:def 3;
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