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

proof

assume A3: x in [.r,q.] \ ].p,s.] ; :: thesis: x in [.r,p.] \/ ].s,q.]
then A4: not x in ].p,s.] by XBOOLE_0:def 5;
A5: r <= x by A3, Th1;
A6: x <= q by A3, Th1;
( not p < x or not x <= s ) by A4, Th2;
then ( x in [.r,p.] or x in ].s,q.] ) by A5, A6, Th1, Th2;
hence x in [.r,p.] \/ ].s,q.] by XBOOLE_0:def 3; :: thesis: verum

end;

assume x in [.r,p.] \/ ].s,q.] ; :: thesis: x in [.r,q.] \ ].p,s.]
then ( x in [.r,p.] or x in ].s,q.] ) by XBOOLE_0:def 3;
then A7: ( ( r <= x & x <= p ) or ( s < x & x <= q ) ) by Th1, Th2;
then A8: r <= x by A1, XXREAL_0:2;
x <= q by A2, A7, XXREAL_0:2;
then A9: x in [.r,q.] by A8, Th1;
not x in ].p,s.] by A7, Th2;
hence x in [.r,q.] \ ].p,s.] by A9, XBOOLE_0:def 5; :: thesis: verum