let p, q, r, s be ExtReal; ( r <= s & p <= q implies [.r,q.] \ [.p,s.[ = [.r,p.[ \/ [.s,q.] )
assume that
A1:
r <= s
and
A2:
p <= q
; [.r,q.] \ [.p,s.[ = [.r,p.[ \/ [.s,q.]
let x be ExtReal; MEMBERED:def 14 ( ( 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.] )
( not x in [.r,p.[ \/ [.s,q.] or x in [.r,q.] \ [.p,s.[ )proof
assume A3:
x in [.r,q.] \ [.p,s.[
;
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, Th3;
then
(
x in [.r,p.[ or
x in [.s,q.] )
by A5, A6, Th1, Th3;
hence
x in [.r,p.[ \/ [.s,q.]
by XBOOLE_0:def 3;
verum
end;
assume
x in [.r,p.[ \/ [.s,q.]
; 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, Th3;
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, Th3;
hence
x in [.r,q.] \ [.p,s.[
by A9, XBOOLE_0:def 5; verum