let e1, e2, e3, e4, e5 be ExtReal; :: thesis: ( e1 <= e2 & e2 <= e3 & e3 <= e4 & e4 <= e5 implies e1 <= e5 )
assume ( e1 <= e2 & e2 <= e3 & e3 <= e4 ) ; :: thesis: ( not e4 <= e5 or e1 <= e5 )
then e1 <= e4 by Th1;
hence ( not e4 <= e5 or e1 <= e5 ) by XXREAL_0:2; :: thesis: verum