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