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

proof

assume t in [.p,r.[ \/ ].s,q.] ; :: thesis: t in [.p,q.]
then ( t in [.p,r.[ or t in ].s,q.] ) by XBOOLE_0:def 3;
then A4: ( ( p <= t & t <= r ) or ( s <= t & t <= q ) ) by Th2, Th3;
then A5: p <= t by A1, XXREAL_0:2;
t <= q by A2, A4, XXREAL_0:2;
hence t in [.p,q.] by A5, Th1; :: thesis: verum

end;

assume t in [.p,q.] ; :: thesis: t in [.p,r.[ \/ ].s,q.]
then ( ( p <= t & t < r ) or ( s < t & t <= q ) ) by A3, Th1, XXREAL_0:2;
then ( t in [.p,r.[ or t in ].s,q.] ) by Th2, Th3;
hence t in [.p,r.[ \/ ].s,q.] by XBOOLE_0:def 3; :: thesis: verum