let r, s, p, q be ext-real number ; :: thesis: ( r <= s & [.r,s.] c= [.p,q.] implies ( p <= r & s <= q ) )
assume r <= s ; :: thesis: ( not [.r,s.] c= [.p,q.] or ( p <= r & s <= q ) )
then ( r in [.r,s.] & s in [.r,s.] ) by Th1;
hence ( not [.r,s.] c= [.p,q.] or ( p <= r & s <= q ) ) by Th1; :: thesis: verum