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;

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 [:{0},REAL+:] ) or ( y in REAL+ & z in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & z in REAL+ ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) )
by A3, A4, NUMBERS:def 1, XBOOLE_0:def 3;

end;

suppose that A5:
x in REAL+
and

A6: y in REAL+ and

A7: z in REAL+ ; :: thesis: x <= z

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 A2, A6, A7, XXREAL_0:def 5;

consider x9, y9 being Element of REAL+ such that

A11: x = x9 and

A12: ( y = y9 & x9 <=' y9 ) by A1, A5, A6, XXREAL_0:def 5;

x9 <=' z9 by A12, A8, A10, ARYTM_1:3;

hence x <= z by A11, A9, XXREAL_0:def 5; :: thesis: verum

end;A8: y = y99 and

A9: z = z9 and

A10: y99 <=' z9 by A2, A6, A7, XXREAL_0:def 5;

consider x9, y9 being Element of REAL+ such that

A11: x = x9 and

A12: ( y = y9 & x9 <=' y9 ) by A1, A5, A6, XXREAL_0:def 5;

x9 <=' z9 by A12, A8, A10, ARYTM_1:3;

hence x <= z by A11, A9, XXREAL_0:def 5; :: thesis: verum

suppose A13:
( x in REAL+ & y in [:{0},REAL+:] )
; :: thesis: x <= z

then
( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) )
by ARYTM_0:5, XBOOLE_0:3;

hence x <= z by A1, A13, XXREAL_0:def 5; :: thesis: verum

end;hence x <= z by A1, A13, XXREAL_0:def 5; :: thesis: verum

suppose A14:
( y in REAL+ & z in [:{0},REAL+:] )
; :: thesis: x <= z

then
( ( not z in REAL+ or not y in REAL+ ) & ( not z in [:{0},REAL+:] or not y in [:{0},REAL+:] ) )
by ARYTM_0:5, XBOOLE_0:3;

hence x <= z by A2, A14, XXREAL_0:def 5; :: thesis: verum

end;hence x <= z by A2, A14, XXREAL_0:def 5; :: thesis: verum

suppose that A15:
x in [:{0},REAL+:]
and

A16: z in REAL+ ; :: thesis: x <= z

A16: z in REAL+ ; :: thesis: x <= z

( ( not x in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] or not z in [:{0},REAL+:] ) )
by A15, A16, ARYTM_0:5, XBOOLE_0:3;

hence x <= z by A16, XXREAL_0:def 5; :: thesis: verum

end;hence x <= z by A16, XXREAL_0:def 5; :: thesis: verum

suppose that A17:
x in [:{0},REAL+:]
and

A18: y in [:{0},REAL+:] and

A19: z in [:{0},REAL+:] ; :: thesis: x <= z

A18: y in [:{0},REAL+:] and

A19: z in [:{0},REAL+:] ; :: 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 A2, A18, A19, XXREAL_0:def 5;

consider x9, y9 being Element of REAL+ such that

A23: x = [0,x9] and

A24: y = [0,y9] and

A25: y9 <=' x9 by A1, A17, A18, XXREAL_0:def 5;

y9 = y99 by A24, A20, XTUPLE_0:1;

then z9 <=' x9 by A25, A22, ARYTM_1:3;

hence x <= z by A17, A19, A23, A21, XXREAL_0:def 5; :: thesis: verum

end;A20: y = [0,y99] and

A21: z = [0,z9] and

A22: z9 <=' y99 by A2, A18, A19, XXREAL_0:def 5;

consider x9, y9 being Element of REAL+ such that

A23: x = [0,x9] and

A24: y = [0,y9] and

A25: y9 <=' x9 by A1, A17, A18, XXREAL_0:def 5;

y9 = y99 by A24, A20, XTUPLE_0:1;

then z9 <=' x9 by A25, A22, ARYTM_1:3;

hence x <= z by A17, A19, A23, A21, XXREAL_0:def 5; :: thesis: verum