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 ) or ( b in REAL+ & c in ) or ( a in & c in REAL+ ) or ( a in & b in & c in ) or ( ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) & ( not a in REAL+ or not b in ) & ( not b in REAL+ or not c in ) & ( not a in or not c in REAL+ ) & ( not a in or not b in or not c in ) ) ) ;
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 ;
hence a <= c by A5, A9, A7, Def5; :: thesis: verum
end;
suppose A11: ( a in REAL+ & b in ) ; :: thesis: a <= c
then ( ( not a in REAL+ or not b in REAL+ ) & ( not a in or not b in ) ) by ;
hence a <= c by A1, A11, Def5, Lm4, Lm5; :: thesis: verum
end;
suppose A12: ( b in REAL+ & c in ) ; :: thesis: a <= c
then ( ( not c in REAL+ or not b in REAL+ ) & ( not c in or not b in ) ) by ;
hence a <= c by A2, A12, Def5, Lm4, Lm5; :: thesis: verum
end;
suppose A13: ( a in & c in REAL+ ) ; :: thesis: a <= c
( ( not a in REAL+ or not c in REAL+ ) & ( not a in or not c in ) ) by ;
hence a <= c by ; :: thesis: verum
end;
suppose that A14: a in and
A15: b in and
A16: c in ; :: 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 ;
then c9 <=' a9 by ;
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 ) and
A25: ( not b in REAL+ or not c in ) and
A26: ( not a in or not c in REAL+ ) and
A27: ( not a in or not b in or not c in ) ; :: thesis: a <= c
A28: ( b = +infty implies c = +infty ) by ;
A29: ( b = -infty implies a = -infty ) by ;
( 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;