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 Th25;
assume ( p <= r & s <= q ) ; :: thesis: ].r,s.[ c= [.p,q.]
then [.r,s.] c= [.p,q.] by Th34;
hence ].r,s.[ c= [.p,q.] by A1, XBOOLE_1:1; :: thesis: verum