let r, s, t be ExtReal; :: thesis: ( r < s & ( for q being ExtReal st r < q & q < s holds
q <= t ) implies s <= t )
assume that
A1: r < s and
A2: for q being ExtReal st r < q & q < s holds
q <= t ; :: thesis: s <= t
for q being ExtReal st t < q holds
s <= q

proof

let q be ExtReal; :: thesis: ( t < q implies s <= q )
assume that
A3: t < q and
A4: q < s ; :: thesis: contradiction

per cases ( r < q or q <= r ) ;

suppose r < q ; :: thesis: contradiction

hence contradiction by A2, A3, A4; :: thesis: verum

end;

suppose A5: q <= r ; :: thesis: contradiction

consider p being ExtReal such that
A6: r < p and
A7: p < s by A1, Th227;
p <= t by A2, A6, A7;
then r <= t by A6, XXREAL_0:2;
hence contradiction by A3, A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence s <= t by Th227; :: thesis: verum