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 )
].r,s.[ c= ].r,s.]
by Th21;
then
].r,s.[ c= [.p,q.]
by A2;
hence
( p <= r & s <= q )
by A1, Th51; verum