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

0 ,one --> a,b = {[0 ,a],[one ,b]} by FUNCT_4:71;
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 set such that
A3: x in {{} } and
y in REAL+ and
A4: 0 ,one --> a,b = [x,y] by ZFMISC_1:103;
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:71;

now

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

A9: now

assume i = j ; :: thesis: contradiction
then {i} = {i,j} by ENUMSET1:69;
then A10: [i,j] = {{i}} by ENUMSET1:69;
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, ZFMISC_1:33; :: 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:9; :: thesis: verum

end;

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

i in [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 ,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:9; :: 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_relative_prime & 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:82;
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

assume 0 ,one --> a,b in omega ; :: thesis: contradiction
then {} in 0 ,one --> a,b by ORDINAL3:10;
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