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

(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 set 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;
then (0,1) --> (a,b) = {{0,y},{0}} by A4, TARSKI:def 5;
then A5: ( [1,b] = {0} or [1,b] = {0,y} ) by A2, TARSKI:def 2;

per cases ( {{1,b},{1}} = {0} or {{1,b},{1}} = {0,y} ) by A5, TARSKI:def 5;

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;

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

now

assume (0,1) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } ; :: thesis: contradiction
then consider i, j being Element of NAT such that
A7: (0,1) --> (a,b) = [i,j] and
i,j are_relative_prime and
j <> {} ;
A8: (0,1) --> (a,b) = {{i,j},{i}} by A7, TARSKI:def 5;
then A9: ( {i} in (0,1) --> (a,b) & {i,j} in (0,1) --> (a,b) ) by TARSKI:def 2;

A10: now

assume i = j ; :: thesis: contradiction
then {i} = {i,j} by ENUMSET1:29;
then A11: [i,j] = {{i}} by A7, A8, ENUMSET1:29;
then [1,b] in {{i}} by A6, A7, TARSKI:def 2;
then A12: [1,b] = {i} by TARSKI:def 1;
[0,a] in {{i}} by A6, A7, A11, TARSKI:def 2;
then [0,a] = {i} by TARSKI:def 1;
hence contradiction by A12, ZFMISC_1:27; :: thesis: verum

end;

A13: [1,b] = {{1,b},{1}} by TARSKI:def 5;
A14: [0,a] = {{0,a},{0}} by TARSKI:def 5;

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 A6, A9, TARSKI:def 2;

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

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

end;

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

i in [0,a] by A15, TARSKI:def 2;
then ( i = {0,a} or i = {0} ) by A14, TARSKI:def 2;
then A17: 0 in i by TARSKI:def 1, TARSKI:def 2;
i = {1} by A16, Lm3;
hence contradiction by A17, TARSKI:def 1; :: thesis: verum

end;

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

i in [1,b] by A18, TARSKI:def 2;
then ( i = {1,b} or i = {1} ) by A13, TARSKI:def 2;
then A20: 1 in i by TARSKI:def 1, TARSKI:def 2;
i = {0} by A19, Lm3;
hence contradiction by A20, TARSKI:def 1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

now

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

end;

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