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 )
].p,q.] c= [.p,q.] by Th23;
then A3: [.r,s.] c= [.p,q.] by A2;
r in [.r,s.] by A1, Th1;
hence p < r by A2, Th2; :: thesis: s <= q
thus s <= q by A1, A3, Th50; :: thesis: verum