let r, s, p, q be ext-real number ; :: thesis: ( r < s & p <= q implies ].r,q.] \ [.p,s.] = ].r,p.[ \/ ].s,q.] )
assume that
Z1: r < s and
Z3: p <= q ; :: thesis: ].r,q.] \ [.p,s.] = ].r,p.[ \/ ].s,q.]
let x be ext-real number ; :: 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 x in ].r,q.] \ [.p,s.] ; :: thesis: x in ].r,p.[ \/ ].s,q.]
then ( x in ].r,q.] & not x in [.p,s.] ) by XBOOLE_0:def 5;
then ( r < x & x <= q & ( not p <= x or not x <= s ) ) by Th2, Th1;
then ( x in ].r,p.[ or x in ].s,q.] ) by Th2, 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 ( ( r < x & x < p ) or ( s < x & x <= q ) ) by Th2, Th4;
then ( r < x & x <= q & ( x < p or s < x ) ) by Z1, Z3, XXREAL_0:2;
then ( x in ].r,q.] & not x in [.p,s.] ) by Th2, Th1;
hence x in ].r,q.] \ [.p,s.] by XBOOLE_0:def 5; :: thesis: verum