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