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
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 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;
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;
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;
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;
suppose that A14: a in [:{0},REAL+:] and
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;
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
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;
end;