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