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 z9 = z as Element of RAT+ by A5;
reconsider y9 = y as Element of RAT+ by A4;
reconsider x9 = x as Element of RAT+ by A3;
( x9 <=' y9 & y9 <=' z9 ) by A1, A2, Lm14;
then x9 <=' z9 by ARYTM_3:67;
hence x <=' z by Lm14; :: thesis: verum
end;
suppose that A6: x in RAT+ and
A7: y in RAT+ and
A8: not z in RAT+ ; :: thesis: x <=' z
reconsider y9 = y as Element of RAT+ by A7;
reconsider x9 = x as Element of RAT+ by A6;
A9: x9 <=' y9 by A1, Lm14;
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 A8, 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 ) ) ;
y in C by A2, A7, A8, A10, Def5;
then x9 in C by A11, A9;
hence x <=' z by A8, A10, Def5; :: thesis: verum
end;
suppose that A12: x in RAT+ and
A13: not y in RAT+ and
A14: z in RAT+ ; :: thesis: x <=' z
reconsider z9 = z as Element of RAT+ by A14;
reconsider x9 = x as Element of RAT+ by A12;
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 A13, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A15: y = B and
A16: 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 ) ) ;
( x9 in B & not z9 in B ) by A1, A2, A13, A15, Def5;
then x9 <=' z9 by A16;
hence x <=' z by Lm14; :: thesis: verum
end;
suppose that A17: x in RAT+ and
A18: not y in RAT+ and
A19: not z in RAT+ ; :: thesis: x <=' z
reconsider x9 = x as Element of RAT+ by A17;
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 A18, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A20: 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 ) ) ;
A21: x9 in B by A1, A18, A20, Def5;
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 A19, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A22: 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 ) ) ;
B c= C by A2, A18, A19, A20, A22, Def5;
hence x <=' z by A19, A22, A21, Def5; :: thesis: verum
end;
suppose that A23: not x in RAT+ and
A24: y in RAT+ and
A25: z in RAT+ ; :: thesis: x <=' z
reconsider z9 = z as Element of RAT+ by A25;
reconsider y9 = y as Element of RAT+ by A24;
A26: y9 <=' z9 by A2, Lm14;
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 A23, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A27: x = A and
A28: 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 ) ) ;
not y9 in A by A1, A23, A27, Def5;
then not z9 in A by A28, A26;
hence x <=' z by A23, A27, Def5; :: thesis: verum
end;
suppose that A29: not x in RAT+ and
A30: y in RAT+ and
A31: 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 A29, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A32: x = A and
A33: 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 ) ) ;
A34: not y in A by A1, A29, A32, Def5;
reconsider y9 = y as Element of RAT+ by A30;
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 A31, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A35: z = C and
A36: 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 ) ) ;
A37: y in C by A2, A30, A31, A35, Def5;
A c= C
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in A or e in C )
assume A38: e in A ; :: thesis: e in C
then reconsider x9 = e as Element of RAT+ ;
x9 <=' y9 by A33, A34, A38;
hence e in C by A36, A37; :: thesis: verum
end;
hence x <=' z by A29, A31, A32, A35, Def5; :: thesis: verum
end;
suppose that A39: not x in RAT+ and
A40: not y in RAT+ and
A41: z in RAT+ ; :: thesis: x <=' z
reconsider z9 = z as Element of RAT+ by A41;
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 A39, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A42: 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 A40, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A43: 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 ) ) ;
A c= B by A1, A39, A40, A42, A43, Def5;
then not z9 in A by A2, A40, A43, Def5;
hence x <=' z by A39, A42, Def5; :: thesis: verum
end;
suppose that A44: not x in RAT+ and
A45: not y in RAT+ and
A46: not z in RAT+ ; :: thesis: x <=' z
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 A46, Lm3, XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A47: 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 ) ) ;
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 A45, Lm3, XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A48: 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 ) ) ;
A49: B c= C by A2, A45, A46, A48, A47, Def5;
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 A44, Lm3, XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A50: 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 ) ) ;
A c= B by A1, A44, A45, A50, A48, Def5;
then A c= C by A49;
hence x <=' z by A44, A46, A50, A47, Def5; :: thesis: verum
end;
end;