let a, b be Element of REAL ; :: thesis: not (0,1) --> (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,1) --> (a,b);

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

(0,1) --> (a,b) = {[0,a],[1,b]} by FUNCT_4:67;
then A2: [1,b] in (0,1) --> (a,b) by TARSKI:def 2;
assume (0,1) --> (a,b) in [:{{}},REAL+:] ; :: thesis: contradiction
then consider x, y being object such that
A3: x in {{}} and
y in REAL+ and
A4: (0,1) --> (a,b) = [x,y] by ZFMISC_1:84;
x = 0 by A3, TARSKI:def 1;

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

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

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

end;

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

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

end;

end;

end;

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

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

assume (0,1) --> (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
A6: (0,1) --> (a,b) = [i,j] and
i,j are_coprime and
j <> {} ;
A7: ( {i} in (0,1) --> (a,b) & {i,j} in (0,1) --> (a,b) ) by A6, TARSKI:def 2;

A8: now :: thesis: not i = j

assume i = j ; :: thesis: contradiction
then {i} = {i,j} by ENUMSET1:29;
then A9: [i,j] = {{i}} by ENUMSET1:29;
then [1,b] in {{i}} by A5, A6, TARSKI:def 2;
then A10: [1,b] = {i} by TARSKI:def 1;
[0,a] in {{i}} by A5, A6, A9, TARSKI:def 2;
then [0,a] = {i} by TARSKI:def 1;
hence contradiction by A10, XTUPLE_0:1; :: thesis: verum

end;

per cases ( ( {i,j} = [0,a] & {i} = [0,a] ) or ( {i,j} = [0,a] & {i} = [1,b] ) or ( {i,j} = [1,b] & {i} = [0,a] ) or ( {i,j} = [1,b] & {i} = [1,b] ) ) by A5, A7, TARSKI:def 2;

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

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

end;

suppose that A11: {i,j} = [0,a] and
A12: {i} = [1,b] ; :: thesis: contradiction

i in {i,j} by TARSKI:def 2;
then ( i = {0,a} or i = {0} ) by A11, TARSKI:def 2;
then A13: 0 in i by TARSKI:def 1, TARSKI:def 2;
i = {1} by A12, Lm4;
hence contradiction by A13, TARSKI:def 1; :: thesis: verum

end;

suppose that A14: {i,j} = [1,b] and
A15: {i} = [0,a] ; :: thesis: contradiction

i in {i,j} by TARSKI:def 2;
then ( i = {1,b} or i = {1} ) by A14, TARSKI:def 2;
then A16: 1 in i by TARSKI:def 1, TARSKI:def 2;
i = {0} by A15, Lm4;
hence contradiction by A16, TARSKI:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

then A17: not (0,1) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of NAT : verum } ;
for x, y being set holds not {[0,x],[1,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 A18: {[0,x],[1,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
A19: {[0,x],[1,y]} = A and
A20: 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 A18;
( [0,x] in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) ) by A19, A20, TARSKI:def 2;
then consider r1, r2, r3 being Element of RAT+ such that
A21: r1 in A and
A22: r2 in A and
A23: ( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) by ARYTM_3:75;
A24: ( r2 = [0,x] or r2 = [1,y] ) by A19, A22, TARSKI:def 2;
( r1 = [0,x] or r1 = [1,y] ) by A19, A21, TARSKI:def 2;
hence contradiction by A19, A23, A24, TARSKI:def 2; :: thesis: verum

end;

then A25: not (0,1) --> (a,b) in DEDEKIND_CUTS by A5, ARYTM_2:def 1;

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

assume (0,1) --> (a,b) in omega ; :: thesis: contradiction
then {} in (0,1) --> (a,b) by ORDINAL3:8;
hence contradiction by A5, TARSKI:def 2; :: thesis: verum

end;

then not (0,1) --> (a,b) in RAT+ by A17, XBOOLE_0:def 3;
then not (0,1) --> (a,b) in REAL+ by A25, ARYTM_2:def 2, XBOOLE_0:def 3;
hence not (0,1) --> (a,b) in REAL by A1, XBOOLE_0:def 3; :: thesis: verum