let a, b, c, d be Real; :: thesis: not (0,1,2,3) --> (a,b,c,d) in REAL
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, FUNCT_4:145;

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

assume (0,1,2,3) --> (a,b,c,d) 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
A2: (0,1,2,3) --> (a,b,c,d) = [i,j] and
i,j are_coprime 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 :: thesis: not i = j

assume i = j ; :: thesis: contradiction
then {i} = {i,j} by ENUMSET1:29;
then A6: [i,j] = {{i}} by ENUMSET1:29;
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, XTUPLE_0:1; :: thesis: verum

end;

per cases ( ( {i} = [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: contradiction

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

end;

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

A12: i = {0} by A10, Lm4;
i in {{1},{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: verum

end;

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

A15: i = {0} by A13, Lm4;
i in {{2},{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: verum

end;

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

A18: i = {0} by A16, Lm4;
i in {{3},{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: verum

end;

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

A21: i = {1} by A19, Lm4;
i in {{0},{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: verum

end;

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

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

end;

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

A24: i = {1} by A22, Lm4;
i in {{2},{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: verum

end;

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

A27: i = {1} by A25, Lm4;
i in {{3},{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: verum

end;

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

A30: i = {2} by A28, Lm4;
i in {{0},{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: verum

end;

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

A33: i = {2} by A31, Lm4;
i in {{1},{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: verum

end;

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

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

end;

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

A36: i = {2} by A34, Lm4;
i in {{3},{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: verum

end;

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

A39: i = {3} by A37, Lm4;
i in {{0},{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: verum

end;

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

A42: i = {3} by A40, Lm4;
i in {{1},{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: verum

end;

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

A45: i = {3} by A43, Lm4;
i in {{2},{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: verum

end;

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

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

end;

end;

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_coprime & j <> {} ) } \ { [k,1] where k is Element of NAT : verum } ;

now :: thesis: not (0,1,2,3) --> (a,b,c,d) in omega

assume (0,1,2,3) --> (a,b,c,d) in omega ; :: thesis: contradiction
then ( not (0,1,2,3) --> (a,b,c,d) is empty & (0,1,2,3) --> (a,b,c,d) is ordinal ) ;
then {} in (0,1,2,3) --> (a,b,c,d) by ORDINAL3:8;
hence contradiction by A1, ENUMSET1:def 2; :: thesis: verum

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 object 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 object 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: contradiction
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, Th3;
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: verum

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 :: thesis: not (0,1,2,3) --> (a,b,c,d) in [:{{}},REAL+:]

assume (0,1,2,3) --> (a,b,c,d) in [:{{}},REAL+:] ; :: thesis: contradiction
then consider x, y being object such that
A71: x in {{}} and
y in REAL+ and
A72: (0,1,2,3) --> (a,b,c,d) = [x,y] by ZFMISC_1:84;
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, FUNCT_4:145;
then A74: [1,b] in (0,1,2,3) --> (a,b,c,d) by ENUMSET1:def 2;

per cases ( {{1,b},{1}} = {0} or {{1,b},{1}} = {0,y} ) by A72, A73, A74, 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;

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