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