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