let x, y, z be Real; :: thesis: ( x <= y & y <= z implies x <= z )
assume that
A1: x <= y and
A2: y <= z ; :: thesis: x <= z
A3: ( x in REAL & y in REAL ) by XREAL_0:def 1;
A4: z in REAL by XREAL_0:def 1;
per cases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in ) or ( y in REAL+ & z in ) or ( x in & z in REAL+ ) or ( x in & y in & z in ) ) by ;
suppose that A5: x in REAL+ and
A6: y in REAL+ and
A7: z in REAL+ ; :: thesis: x <= z
consider y99, z9 being Element of REAL+ such that
A8: y = y99 and
A9: z = z9 and
A10: y99 <=' z9 by ;
consider x9, y9 being Element of REAL+ such that
A11: x = x9 and
A12: ( y = y9 & x9 <=' y9 ) by ;
x9 <=' z9 by ;
hence x <= z by ; :: thesis: verum
end;
suppose A13: ( x in REAL+ & y in ) ; :: thesis: x <= z
then ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) ) by ;
hence x <= z by ; :: thesis: verum
end;
suppose A14: ( y in REAL+ & z in ) ; :: thesis: x <= z
then ( ( not z in REAL+ or not y in REAL+ ) & ( not z in or not y in ) ) by ;
hence x <= z by ; :: thesis: verum
end;
suppose that A15: x in and
A16: z in REAL+ ; :: thesis: x <= z
( ( not x in REAL+ or not z in REAL+ ) & ( not x in or not z in ) ) by ;
hence x <= z by ; :: thesis: verum
end;
suppose that A17: x in and
A18: y in and
A19: z in ; :: thesis: x <= z
consider y99, z9 being Element of REAL+ such that
A20: y = [0,y99] and
A21: z = [0,z9] and
A22: z9 <=' y99 by ;
consider x9, y9 being Element of REAL+ such that
A23: x = [0,x9] and
A24: y = [0,y9] and
A25: y9 <=' x9 by ;
y9 = y99 by ;
then z9 <=' x9 by ;
hence x <= z by ; :: thesis: verum
end;
end;