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