let x, y, z be Element of REAL+ ; :: thesis: ( x <=' y & y <=' z implies x <=' z )
assume that
A1: x <=' y and
A2: y <=' z ; :: thesis: x <=' z

per cases ( ( x in RAT+ & y in RAT+ & z in RAT+ ) or ( x in RAT+ & y in RAT+ & not z in RAT+ ) or ( x in RAT+ & not y in RAT+ & z in RAT+ ) or ( x in RAT+ & not y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & y in RAT+ & z in RAT+ ) or ( not x in RAT+ & y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & not z in RAT+ ) ) ;

suppose that A3: x in RAT+ and
A4: y in RAT+ and
A5: z in RAT+ ; :: thesis: x <=' z

reconsider x' = x as Element of RAT+ by A3;
reconsider y' = y as Element of RAT+ by A4;
reconsider z' = z as Element of RAT+ by A5;
A6: x' <=' y' by A1, Lm14;
y' <=' z' by A2, Lm14;
then x' <=' z' by A6, ARYTM_3:74;
hence x <=' z by Lm14; :: thesis: verum

end;

suppose that A7: x in RAT+ and
A8: y in RAT+ and
A9: not z in RAT+ ; :: thesis: x <=' z

reconsider x' = x as Element of RAT+ by A7;
reconsider y' = y as Element of RAT+ by A8;
z in REAL+ ;
then z 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 ) ) } by A9, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A10: z = C and
A11: for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
A12: x' <=' y' by A1, Lm14;
y in C by A2, A8, A9, A10, Def5;
then x' in C by A11, A12;
hence x <=' z by A9, A10, Def5; :: thesis: verum

end;

suppose that A13: x in RAT+ and
A14: not y in RAT+ and
A15: z in RAT+ ; :: thesis: x <=' z

reconsider x' = x as Element of RAT+ by A13;
y in REAL+ ;
then 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 ) ) } by A14, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A16: y = B and
A17: for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
reconsider z' = z as Element of RAT+ by A15;
A18: x' in B by A1, A14, A16, Def5;
not z' in B by A2, A14, A16, Def5;
then x' <=' z' by A17, A18;
hence x <=' z by Lm14; :: thesis: verum

end;

suppose that A19: x in RAT+ and
A20: not y in RAT+ and
A21: not z in RAT+ ; :: thesis: x <=' z

reconsider x' = x as Element of RAT+ by A19;
y in REAL+ ;
then 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 ) ) } by A20, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A22: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
z in REAL+ ;
then z 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 ) ) } by A21, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A23: z = C and
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
A24: x' in B by A1, A20, A22, Def5;
B c= C by A2, A20, A21, A22, A23, Def5;
hence x <=' z by A21, A23, A24, Def5; :: thesis: verum

end;

suppose that A25: not x in RAT+ and
A26: y in RAT+ and
A27: z in RAT+ ; :: thesis: x <=' z

x in REAL+ ;
then x 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 ) ) } by A25, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A28: x = A and
A29: 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 ) ) ;
reconsider y' = y as Element of RAT+ by A26;
reconsider z' = z as Element of RAT+ by A27;
A30: not y' in A by A1, A25, A28, Def5;
y' <=' z' by A2, Lm14;
then not z' in A by A29, A30;
hence x <=' z by A25, A28, Def5; :: thesis: verum

end;

suppose that A31: not x in RAT+ and
A32: y in RAT+ and
A33: not z in RAT+ ; :: thesis: x <=' z

x in REAL+ ;
then x 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 ) ) } by A31, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A34: x = A and
A35: 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 ) ) ;
reconsider y' = y as Element of RAT+ by A32;
z in REAL+ ;
then z 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 ) ) } by A33, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A36: z = C and
A37: for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
A38: not y in A by A1, A31, A34, Def5;
A39: y in C by A2, A32, A33, A36, Def5;
A c= C

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in A or e in C )
assume A40: e in A ; :: thesis: e in C
then reconsider x' = e as Element of RAT+ ;
x' <=' y' by A35, A38, A40;
hence e in C by A37, A39; :: thesis: verum

end;

hence x <=' z by A31, A33, A34, A36, Def5; :: thesis: verum

end;

suppose that A41: not x in RAT+ and
A42: not y in RAT+ and
A43: z in RAT+ ; :: thesis: x <=' z

x in REAL+ ;
then x 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 ) ) } by A41, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A44: x = A and
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 ) ) ;
y in REAL+ ;
then 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 ) ) } by A42, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A45: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
reconsider z' = z as Element of RAT+ by A43;
A c= B by A1, A41, A42, A44, A45, Def5;
then not z' in A by A2, A42, A45, Def5;
hence x <=' z by A41, A44, Def5; :: thesis: verum

end;

suppose that A46: not x in RAT+ and
A47: not y in RAT+ and
A48: not z in RAT+ ; :: thesis: x <=' z

x in REAL+ ;
then x 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 ) ) } by A46, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A49: x = A and
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 ) ) ;
y in REAL+ ;
then 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 ) ) } by A47, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A50: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
z in REAL+ ;
then z 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 ) ) } by A48, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A51: z = C and
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
A52: A c= B by A1, A46, A47, A49, A50, Def5;
B c= C by A2, A47, A48, A50, A51, Def5;
then A c= C by A52, XBOOLE_1:1;
hence x <=' z by A46, A48, A49, A51, Def5; :: thesis: verum

end;

end;