let p, q, r, s be ExtReal; :: thesis: ( r < s & [.r,s.[ c= [.p,q.[ implies ( p <= r & s <= q ) )
assume that
A1: r < s and
A2: [.r,s.[ c= [.p,q.[ ; :: thesis: ( p <= r & s <= q )
].r,s.[ c= [.r,s.[ by Th22;
then A3: ].r,s.[ c= [.p,q.[ by A2;
[.p,q.[ c= [.p,q.] by Th24;
then ].r,s.[ c= [.p,q.] by A3;
hence ( p <= r & s <= q ) by A1, Th51; :: thesis: verum