let r, s, t be ExtReal; ( 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
; t <= r
for q being ExtReal st r < q holds
t <= q
hence
t <= r
by Th227; verum