let r, s, t be Real; :: thesis:
assume that
A1: r <= s and
A2: s <= t ; :: thesis:
A3: ( r in REAL & s in REAL ) by Def1;
A4: t in REAL by Def1;

per cases by A3, A4, NUMBERS:def 1, XBOOLE_0:def 3;

suppose that A5: r in REAL+ and
A6: s in REAL+ and
A7: t in REAL+ ; :: thesis:

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:

end;

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

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:

end;

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

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:

end;

suppose that A15: r in [:{0},REAL+:] and
A16: t in REAL+ ; :: thesis:

( ( 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:

end;

suppose that A17: r in [:{0},REAL+:] and
A18: s in [:{0},REAL+:] and
A19: t in [:{0},REAL+:] ; :: thesis:

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:

end;

end;