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

proof

let q be ExtReal; :: thesis: ( r < q implies t <= q )
assume A3: r < q ; :: thesis: t <= q

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

suppose q < s ; :: thesis: t <= q

hence t <= q by A2, A3; :: thesis: verum

end;

suppose A4: s <= q ; :: thesis: t <= q

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

end;

end;

end;

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