let a, b, c be ext-real number ; :: thesis: ( a <= b & b <= c implies a <= c )
assume that
A1: a <= b and
A2: b <= c ; :: thesis: a <= c

per cases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in REAL+ & b in [:{0 },REAL+ :] ) or ( b in REAL+ & c in [:{0 },REAL+ :] ) or ( a in [:{0 },REAL+ :] & c in REAL+ ) or ( a in [:{0 },REAL+ :] & b in [:{0 },REAL+ :] & c in [:{0 },REAL+ :] ) or ( ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) & ( not a in REAL+ or not b in [:{0 },REAL+ :] ) & ( not b in REAL+ or not c in [:{0 },REAL+ :] ) & ( not a in [:{0 },REAL+ :] or not c in REAL+ ) & ( not a in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] or not c in [:{0 },REAL+ :] ) ) ) ;

suppose that A3: a in REAL+ and
A4: b in REAL+ and
A5: c in REAL+ ; :: thesis: a <= c

consider a', b' being Element of REAL+ such that
A6: a = a' and
A7: b = b' and
A8: a' <=' b' by A1, A3, A4, Def5;
consider b'', c' being Element of REAL+ such that
A9: b = b'' and
A10: c = c' and
A11: b'' <=' c' by A2, A4, A5, Def5;
a' <=' c' by A7, A8, A9, A11, ARYTM_1:3;
hence a <= c by A5, A6, A10, Def5; :: thesis: verum

end;

suppose A12: ( a in REAL+ & b in [:{0 },REAL+ :] ) ; :: thesis: a <= c

then ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence a <= c by A1, A12, Def5, Lm3, Lm4; :: thesis: verum

end;

suppose A13: ( b in REAL+ & c in [:{0 },REAL+ :] ) ; :: thesis: a <= c

then ( ( not c in REAL+ or not b in REAL+ ) & ( not c in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence a <= c by A2, A13, Def5, Lm3, Lm4; :: thesis: verum

end;

suppose that A14: a in [:{0 },REAL+ :] and
A15: c in REAL+ ; :: thesis: a <= c

( ( not a in REAL+ or not c in REAL+ ) & ( not a in [:{0 },REAL+ :] or not c in [:{0 },REAL+ :] ) ) by A14, A15, ARYTM_0:5, XBOOLE_0:3;
hence a <= c by A14, A15, Def5; :: thesis: verum

end;

suppose that A16: a in [:{0 },REAL+ :] and
A17: b in [:{0 },REAL+ :] and
A18: c in [:{0 },REAL+ :] ; :: thesis: a <= c

consider a', b' being Element of REAL+ such that
A19: a = [0 ,a'] and
A20: b = [0 ,b'] and
A21: b' <=' a' by A1, A16, A17, Def5;
consider b'', c' being Element of REAL+ such that
A22: b = [0 ,b''] and
A23: c = [0 ,c'] and
A24: c' <=' b'' by A2, A17, A18, Def5;
b' = b'' by A20, A22, ZFMISC_1:33;
then c' <=' a' by A21, A24, ARYTM_1:3;
hence a <= c by A16, A18, A19, A23, Def5; :: thesis: verum

end;

suppose that A25: ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) and
A26: ( not a in REAL+ or not b in [:{0 },REAL+ :] ) and
A27: ( not b in REAL+ or not c in [:{0 },REAL+ :] ) and
A28: ( not a in [:{0 },REAL+ :] or not c in REAL+ ) and
A29: ( not a in [:{0 },REAL+ :] or not b in [:{0 },REAL+ :] or not c in [:{0 },REAL+ :] ) ; :: thesis: a <= c

A30: ( b = +infty implies c = +infty ) by A2, Lm8;
A31: ( b = -infty implies a = -infty ) by A1, Lm7;
( a = -infty or b = +infty or b = -infty or c = +infty ) by A1, A2, A25, A27, A28, A29, Def5;
hence a <= c by A1, A2, A25, A26, A27, A29, A30, A31, Def5; :: thesis: verum

end;

end;