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 Th4, Th3;
then ( x in [.r,p.] or x in [.s,q.[ ) by Th3, Th1;
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 Th3, Th1;
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 Th4, Th3;
hence x in [.r,q.[ \ ].p,s.[ by XBOOLE_0:def 5; :: thesis: verum