let p, q, r, s be ExtReal; :: thesis: ( r >= p & s > q implies [.r,s.[ /\ [.p,q.] = [.r,q.] )
assume that
A1: r >= p and
A2: s > q ; :: thesis: [.r,s.[ /\ [.p,q.] = [.r,q.]
let t be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not t in [.r,s.[ /\ [.p,q.] or t in [.r,q.] ) & ( not t in [.r,q.] or t in [.r,s.[ /\ [.p,q.] ) )
thus ( t in [.r,s.[ /\ [.p,q.] implies t in [.r,q.] ) :: thesis: ( not t in [.r,q.] or t in [.r,s.[ /\ [.p,q.] )

proof

assume A3: t in [.r,s.[ /\ [.p,q.] ; :: thesis: t in [.r,q.]
then A4: t in [.r,s.[ by XBOOLE_0:def 4;
A5: t in [.p,q.] by A3, XBOOLE_0:def 4;
A6: r <= t by A4, Th3;
t <= q by A5, Th1;
hence t in [.r,q.] by A6, Th1; :: thesis: verum

end;

assume A7: t in [.r,q.] ; :: thesis: t in [.r,s.[ /\ [.p,q.]
then A8: r <= t by Th1;
A9: t <= q by A7, Th1;
then A10: t < s by A2, XXREAL_0:2;
A11: p <= t by A1, A8, XXREAL_0:2;
A12: t in [.r,s.[ by A8, A10, Th3;
t in [.p,q.] by A9, A11, Th1;
hence t in [.r,s.[ /\ [.p,q.] by A12, XBOOLE_0:def 4; :: thesis: verum