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 Th25;
then A3: [.r,s.[ c= [.p,q.] by A2, XBOOLE_1:1;
r in [.r,s.[ by A1, Th3;
hence p < r by A2, Th4; :: thesis: s <= q
thus s <= q by A1, A3, Th52; :: thesis: verum