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