let a, b, c be ExtReal; :: thesis: ( a <= b & b <= c implies a <= c )

assume that

A1: a <= b and

A2: b <= c ; :: thesis: 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+:] ) ) )
;

end;

suppose that A3:
a in REAL+
and

A4: b in REAL+ and

A5: c in REAL+ ; :: thesis: a <= c

A4: b in REAL+ and

A5: c in REAL+ ; :: thesis: a <= c

consider b99, c9 being Element of REAL+ such that

A6: b = b99 and

A7: c = c9 and

A8: b99 <=' c9 by A2, A4, A5, Def5;

consider a9, b9 being Element of REAL+ such that

A9: a = a9 and

A10: ( b = b9 & a9 <=' b9 ) by A1, A3, A4, Def5;

a9 <=' c9 by A10, A6, A8, ARYTM_1:3;

hence a <= c by A5, A9, A7, Def5; :: thesis: verum

end;A6: b = b99 and

A7: c = c9 and

A8: b99 <=' c9 by A2, A4, A5, Def5;

consider a9, b9 being Element of REAL+ such that

A9: a = a9 and

A10: ( b = b9 & a9 <=' b9 ) by A1, A3, A4, Def5;

a9 <=' c9 by A10, A6, A8, ARYTM_1:3;

hence a <= c by A5, A9, A7, Def5; :: thesis: verum

suppose A11:
( 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, A11, Def5, Lm4, Lm5; :: thesis: verum

end;hence a <= c by A1, A11, Def5, Lm4, Lm5; :: thesis: verum

suppose A12:
( 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, A12, Def5, Lm4, Lm5; :: thesis: verum

end;hence a <= c by A2, A12, Def5, Lm4, Lm5; :: thesis: verum

suppose A13:
( a in [:{0},REAL+:] & 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 A13, ARYTM_0:5, XBOOLE_0:3;

hence a <= c by A13, Def5; :: thesis: verum

end;hence a <= c by A13, Def5; :: thesis: verum

suppose that A14:
a in [:{0},REAL+:]
and

A15: b in [:{0},REAL+:] and

A16: c in [:{0},REAL+:] ; :: thesis: a <= c

A15: b in [:{0},REAL+:] and

A16: c in [:{0},REAL+:] ; :: thesis: a <= c

consider b99, c9 being Element of REAL+ such that

A17: b = [0,b99] and

A18: c = [0,c9] and

A19: c9 <=' b99 by A2, A15, A16, Def5;

consider a9, b9 being Element of REAL+ such that

A20: a = [0,a9] and

A21: b = [0,b9] and

A22: b9 <=' a9 by A1, A14, A15, Def5;

b9 = b99 by A21, A17, XTUPLE_0:1;

then c9 <=' a9 by A22, A19, ARYTM_1:3;

hence a <= c by A14, A16, A20, A18, Def5; :: thesis: verum

end;A17: b = [0,b99] and

A18: c = [0,c9] and

A19: c9 <=' b99 by A2, A15, A16, Def5;

consider a9, b9 being Element of REAL+ such that

A20: a = [0,a9] and

A21: b = [0,b9] and

A22: b9 <=' a9 by A1, A14, A15, Def5;

b9 = b99 by A21, A17, XTUPLE_0:1;

then c9 <=' a9 by A22, A19, ARYTM_1:3;

hence a <= c by A14, A16, A20, A18, Def5; :: thesis: verum

suppose that A23:
( not a in REAL+ or not b in REAL+ or not c in REAL+ )
and

A24: ( not a in REAL+ or not b in [:{0},REAL+:] ) and

A25: ( not b in REAL+ or not c in [:{0},REAL+:] ) and

A26: ( not a in [:{0},REAL+:] or not c in REAL+ ) and

A27: ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ; :: thesis: a <= c

A24: ( not a in REAL+ or not b in [:{0},REAL+:] ) and

A25: ( not b in REAL+ or not c in [:{0},REAL+:] ) and

A26: ( not a in [:{0},REAL+:] or not c in REAL+ ) and

A27: ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ; :: thesis: a <= c

A28:
( b = +infty implies c = +infty )
by A2, Lm9;

A29: ( b = -infty implies a = -infty ) by A1, Lm8;

( a = -infty or b = +infty or b = -infty or c = +infty ) by A1, A2, A23, A25, A26, A27, Def5;

hence a <= c by A1, A2, A23, A24, A25, A27, A28, A29, Def5; :: thesis: verum

end;A29: ( b = -infty implies a = -infty ) by A1, Lm8;

( a = -infty or b = +infty or b = -infty or c = +infty ) by A1, A2, A23, A25, A26, A27, Def5;

hence a <= c by A1, A2, A23, A24, A25, A27, A28, A29, Def5; :: thesis: verum