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