let r, s, p, q be ext-real number ; :: thesis: ( r < s & ].r,s.[ c= ].p,q.] implies ( p <= r & s <= q ) )
assume that
A1: r < s and
A2: ].r,s.[ c= ].p,q.] ; :: thesis: ( p <= r & s <= q )
].p,q.] c= [.p,q.] by Th23;
then ].r,s.[ c= [.p,q.] by A2, XBOOLE_1:1;
hence ( p <= r & s <= q ) by A1, Th51; :: thesis: verum