let r, s, t be Real; :: thesis: ( r <= s & s <= t implies r <= t )

assume that

A1: r <= s and

A2: s <= t ; :: thesis: r <= t

A3: ( r in REAL & s in REAL ) by Def1;

A4: t in REAL by Def1;

assume that

A1: r <= s and

A2: s <= t ; :: thesis: r <= t

A3: ( r in REAL & s in REAL ) by Def1;

A4: t in REAL by Def1;

per cases
( ( r in REAL+ & s in REAL+ & t in REAL+ ) or ( r in REAL+ & s in [:{0},REAL+:] ) or ( s in REAL+ & t in [:{0},REAL+:] ) or ( r in [:{0},REAL+:] & t in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & t in [:{0},REAL+:] ) )
by A3, A4, NUMBERS:def 1, XBOOLE_0:def 3;

end;

suppose that A5:
r in REAL+
and

A6: s in REAL+ and

A7: t in REAL+ ; :: thesis: r <= t

A6: s in REAL+ and

A7: t in REAL+ ; :: thesis: r <= t

consider s99, t9 being Element of REAL+ such that

A8: s = s99 and

A9: t = t9 and

A10: s99 <=' t9 by A2, A6, A7, XXREAL_0:def 5;

consider x9, s9 being Element of REAL+ such that

A11: r = x9 and

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

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

hence r <= t by A11, A9, Lm2; :: thesis: verum

end;A8: s = s99 and

A9: t = t9 and

A10: s99 <=' t9 by A2, A6, A7, XXREAL_0:def 5;

consider x9, s9 being Element of REAL+ such that

A11: r = x9 and

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

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

hence r <= t by A11, A9, Lm2; :: thesis: verum

suppose A13:
( r in REAL+ & s in [:{0},REAL+:] )
; :: thesis: r <= t

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

hence r <= t by A1, A13, XXREAL_0:def 5; :: thesis: verum

end;hence r <= t by A1, A13, XXREAL_0:def 5; :: thesis: verum

suppose A14:
( s in REAL+ & t in [:{0},REAL+:] )
; :: thesis: r <= t

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

hence r <= t by A2, A14, XXREAL_0:def 5; :: thesis: verum

end;hence r <= t by A2, A14, XXREAL_0:def 5; :: thesis: verum

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

A16: t in REAL+ ; :: thesis: r <= t

A16: t in REAL+ ; :: thesis: r <= t

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

hence r <= t by A16, XXREAL_0:def 5; :: thesis: verum

end;hence r <= t by A16, XXREAL_0:def 5; :: thesis: verum

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

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

A19: t in [:{0},REAL+:] ; :: thesis: r <= t

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

A19: t in [:{0},REAL+:] ; :: thesis: r <= t

consider s99, t9 being Element of REAL+ such that

A20: s = [0,s99] and

A21: t = [0,t9] and

A22: t9 <=' s99 by A2, A18, A19, XXREAL_0:def 5;

consider x9, s9 being Element of REAL+ such that

A23: r = [0,x9] and

A24: s = [0,s9] and

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

s9 = s99 by A24, A20, XTUPLE_0:1;

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

hence r <= t by A17, A19, A23, A21, Lm2; :: thesis: verum

end;A20: s = [0,s99] and

A21: t = [0,t9] and

A22: t9 <=' s99 by A2, A18, A19, XXREAL_0:def 5;

consider x9, s9 being Element of REAL+ such that

A23: r = [0,x9] and

A24: s = [0,s9] and

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

s9 = s99 by A24, A20, XTUPLE_0:1;

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

hence r <= t by A17, A19, A23, A21, Lm2; :: thesis: verum