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 Real; :: according to MEMBERED:def 15 :: 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, Th4;
A6: x < q by A3, Th4;
( not p <= x or not x <= s ) by A4, Th1;
then ( x in ].r,p.[ or x in ].s,q.[ ) by A5, A6, Th4;
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 Th4;
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, Th4;
not x in [.p,s.] by A7, Th1;
hence x in ].r,q.[ \ [.p,s.] by A9, XBOOLE_0:def 5; :: thesis: verum