let a, b, c, d be Element of REAL ; :: thesis:
set f = 0 ,1,2,3 --> a,b,c,d;
A1: 0 ,1,2,3 --> a,b,c,d = {[0 ,a],[1,b],[2,c],[3,d]} by Lm1, Th8;

assume 0 ,1,2,3 --> a,b,c,d in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } ; :: thesis:
then consider i, j being Element of NAT such that
A2: 0 ,1,2,3 --> a,b,c,d = [i,j] and
i,j are_relative_prime and
j <> {} ;
A3: {i} in 0 ,1,2,3 --> a,b,c,d by A2, TARSKI:def 2;
A4: {i,j} in 0 ,1,2,3 --> a,b,c,d by A2, TARSKI:def 2;

A5: now

assume i = j ; :: thesis:
then {i} = {i,j} by ENUMSET1:69;
then A6: [i,j] = {{i}} by ENUMSET1:69;
then A7: [0 ,a] in {{i}} by A1, A2, ENUMSET1:def 2;
A8: [1,b] in {{i}} by A1, A2, A6, ENUMSET1:def 2;
A9: [0 ,a] = {i} by A7, TARSKI:def 1;
[1,b] = {i} by A8, TARSKI:def 1;
hence contradiction by A9, ZFMISC_1:33; :: thesis:

end;

per cases = [0 ,a] & {i,j} = [0 ,a] ) or ( {i} = [0 ,a] & {i,j} = [1,b] ) or ( {i} = [0 ,a] & {i,j} = [2,c] ) or ( {i} = [0 ,a] & {i,j} = [3,d] ) or ( {i} = [1,b] & {i,j} = [0 ,a] ) or ( {i} = [1,b] & {i,j} = [1,b] ) or ( {i} = [1,b] & {i,j} = [2,c] ) or ( {i} = [1,b] & {i,j} = [3,d] ) or ( {i} = [2,c] & {i,j} = [0 ,a] ) or ( {i} = [2,c] & {i,j} = [1,b] ) or ( {i} = [2,c] & {i,j} = [2,c] ) or ( {i} = [2,c] & {i,j} = [3,d] ) or ( {i} = [3,d] & {i,j} = [0 ,a] ) or ( {i} = [3,d] & {i,j} = [1,b] ) or ( {i} = [3,d] & {i,j} = [2,c] ) or ( {i} = [3,d] & {i,j} = [3,d] ) ) by A1, A3, A4, ENUMSET1:def 2;

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

hence contradiction by A5, ZFMISC_1:9; :: thesis:

end;

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

A12: i = {0 } by A10, Lm5;
i in [1,b] by A11, TARSKI:def 2;
then ( i = {1,b} or i = {1} ) by TARSKI:def 2;
then 1 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A12, TARSKI:def 1; :: thesis:

end;

suppose that A13: {i} = [0 ,a] and
A14: {i,j} = [2,c] ; :: thesis:

A15: i = {0 } by A13, Lm5;
i in [2,c] by A14, TARSKI:def 2;
then ( i = {2,c} or i = {2} ) by TARSKI:def 2;
then 2 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A15, TARSKI:def 1; :: thesis:

end;

suppose that A16: {i} = [0 ,a] and
A17: {i,j} = [3,d] ; :: thesis:

A18: i = {0 } by A16, Lm5;
i in [3,d] by A17, TARSKI:def 2;
then ( i = {3,d} or i = {3} ) by TARSKI:def 2;
then 3 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A18, TARSKI:def 1; :: thesis:

end;

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

A21: i = {1} by A19, Lm5;
i in [0 ,a] by A20, TARSKI:def 2;
then ( i = {0 ,a} or i = {0 } ) by TARSKI:def 2;
then 0 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A21, TARSKI:def 1; :: thesis:

end;

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

hence contradiction by A5, ZFMISC_1:9; :: thesis:

end;

suppose that A22: {i} = [1,b] and
A23: {i,j} = [2,c] ; :: thesis:

A24: i = {1} by A22, Lm5;
i in [2,c] by A23, TARSKI:def 2;
then ( i = {2,c} or i = {2} ) by TARSKI:def 2;
then 2 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A24, TARSKI:def 1; :: thesis:

end;

suppose that A25: {i} = [1,b] and
A26: {i,j} = [3,d] ; :: thesis:

A27: i = {1} by A25, Lm5;
i in [3,d] by A26, TARSKI:def 2;
then ( i = {3,d} or i = {3} ) by TARSKI:def 2;
then 3 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A27, TARSKI:def 1; :: thesis:

end;

suppose that A28: {i} = [2,c] and
A29: {i,j} = [0 ,a] ; :: thesis:

A30: i = {2} by A28, Lm5;
i in [0 ,a] by A29, TARSKI:def 2;
then ( i = {0 ,a} or i = {0 } ) by TARSKI:def 2;
then 0 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A30, TARSKI:def 1; :: thesis:

end;

suppose that A31: {i} = [2,c] and
A32: {i,j} = [1,b] ; :: thesis:

A33: i = {2} by A31, Lm5;
i in [1,b] by A32, TARSKI:def 2;
then ( i = {1,b} or i = {1} ) by TARSKI:def 2;
then 1 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A33, TARSKI:def 1; :: thesis:

end;

suppose ( {i} = [2,c] & {i,j} = [2,c] ) ; :: thesis:

hence contradiction by A5, ZFMISC_1:9; :: thesis:

end;

suppose that A34: {i} = [2,c] and
A35: {i,j} = [3,d] ; :: thesis:

A36: i = {2} by A34, Lm5;
i in [3,d] by A35, TARSKI:def 2;
then ( i = {3,d} or i = {3} ) by TARSKI:def 2;
then 3 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A36, TARSKI:def 1; :: thesis:

end;

suppose that A37: {i} = [3,d] and
A38: {i,j} = [0 ,a] ; :: thesis:

A39: i = {3} by A37, Lm5;
i in [0 ,a] by A38, TARSKI:def 2;
then ( i = {0 ,a} or i = {0 } ) by TARSKI:def 2;
then 0 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A39, TARSKI:def 1; :: thesis:

end;

suppose that A40: {i} = [3,d] and
A41: {i,j} = [1,b] ; :: thesis:

A42: i = {3} by A40, Lm5;
i in [1,b] by A41, TARSKI:def 2;
then ( i = {1,b} or i = {1} ) by TARSKI:def 2;
then 1 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A42, TARSKI:def 1; :: thesis:

end;

suppose that A43: {i} = [3,d] and
A44: {i,j} = [2,c] ; :: thesis:

A45: i = {3} by A43, Lm5;
i in [2,c] by A44, TARSKI:def 2;
then ( i = {2,c} or i = {2} ) by TARSKI:def 2;
then 2 in i by TARSKI:def 1, TARSKI:def 2;
hence contradiction by A45, TARSKI:def 1; :: thesis:

end;

suppose ( {i} = [3,d] & {i,j} = [3,d] ) ; :: thesis:

hence contradiction by A5, ZFMISC_1:9; :: thesis:

end;

then A46: not 0 ,1,2,3 --> a,b,c,d 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 } ;

now

assume 0 ,1,2,3 --> a,b,c,d in omega ; :: thesis:
then {} in 0 ,1,2,3 --> a,b,c,d by ORDINAL3:10;
hence contradiction by A1, ENUMSET1:def 2; :: thesis:

end;

then A47: not 0 ,1,2,3 --> a,b,c,d in RAT+ by A46, XBOOLE_0:def 3;
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 ) ) } ;
for x, y, z, w being set holds not {[0 ,x],[1,y],[2,z],[3,w]} 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, z, w being set such that A48: {[0 ,x],[1,y],[2,z],[3,w]} 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:
consider A being Subset of RAT+ such that
A49: {[0 ,x],[1,y],[2,z],[3,w]} = A and
A50: 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 A48;
A51: [0 ,x] in A by A49, ENUMSET1:def 2;
for r, s being Element of RAT+ st r in A & s <=' r holds
s in A by A50;
then consider r1, r2, r3, r4, r5 being Element of RAT+ such that
A52: r1 in A and
A53: r2 in A and
A54: r3 in A and
A55: r4 in A and
A56: r5 in A and
A57: r1 <> r2 and
A58: r1 <> r3 and
A59: r1 <> r4 and
A60: r1 <> r5 and
A61: r2 <> r3 and
A62: r2 <> r4 and
A63: r2 <> r5 and
A64: r3 <> r4 and
A65: r3 <> r5 and
A66: r4 <> r5 by A51, Th9;
A67: ( r1 = [0 ,x] or r1 = [1,y] or r1 = [2,z] or r1 = [3,w] ) by A49, A52, ENUMSET1:def 2;
A68: ( r2 = [0 ,x] or r2 = [1,y] or r2 = [2,z] or r2 = [3,w] ) by A49, A53, ENUMSET1:def 2;
A69: ( r3 = [0 ,x] or r3 = [1,y] or r3 = [2,z] or r3 = [3,w] ) by A49, A54, ENUMSET1:def 2;
( r4 = [0 ,x] or r4 = [1,y] or r4 = [2,z] or r4 = [3,w] ) by A49, A55, ENUMSET1:def 2;
hence contradiction by A49, A56, A57, A58, A59, A60, A61, A62, A63, A64, A65, A66, A67, A68, A69, ENUMSET1:def 2; :: thesis:

end;

then not 0 ,1,2,3 --> a,b,c,d in DEDEKIND_CUTS by A1, ARYTM_2:def 1;
then A70: not 0 ,1,2,3 --> a,b,c,d in REAL+ by A47, ARYTM_2:def 2, XBOOLE_0:def 3;

now

assume 0 ,1,2,3 --> a,b,c,d in [:{{} },REAL+ :] ; :: thesis:
then consider x, y being set such that
A71: x in {{} } and
y in REAL+ and
A72: 0 ,1,2,3 --> a,b,c,d = [x,y] by ZFMISC_1:103;
A73: x = 0 by A71, TARSKI:def 1;
0 ,1,2,3 --> a,b,c,d = {[0 ,a],[1,b],[2,c],[3,d]} by Lm1, Th8;
then A74: [1,b] in 0 ,1,2,3 --> a,b,c,d by ENUMSET1:def 2;

per cases = {0 } or {{1,b},{1}} = {0 ,y} ) by A72, A73, A74, TARSKI:def 2;

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

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

end;

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

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

end;

hence not 0 ,1,2,3 --> a,b,c,d in REAL by A70, NUMBERS:def 1, XBOOLE_0:def 3; :: thesis: