let p, q, r, s be ExtReal; ( r < s & ].r,s.[ c= [.p,q.[ implies ( p <= r & s <= q ) )
assume that
A1:
r < s
and
A2:
].r,s.[ c= [.p,q.[
; ( p <= r & s <= q )
[.p,q.[ c= [.p,q.]
by Th24;
then
].r,s.[ c= [.p,q.]
by A2;
hence
( p <= r & s <= q )
by A1, Th51; verum