let p, q, r, s be ExtReal; ( p < s & r <= q & s <= r implies ].p,r.] \/ [.s,q.] = ].p,q.] )
assume that
A1:
p < s
and
A2:
r <= q
and
A3:
s <= r
; ].p,r.] \/ [.s,q.] = ].p,q.]
let t be ExtReal; MEMBERED:def 14 ( ( not t in ].p,r.] \/ [.s,q.] or t in ].p,q.] ) & ( not t in ].p,q.] or t in ].p,r.] \/ [.s,q.] ) )
thus
( t in ].p,r.] \/ [.s,q.] implies t in ].p,q.] )
( not t in ].p,q.] or t in ].p,r.] \/ [.s,q.] )proof
assume
t in ].p,r.] \/ [.s,q.]
;
t in ].p,q.]
then
(
t in ].p,r.] or
t in [.s,q.] )
by XBOOLE_0:def 3;
then A4:
( (
p < t &
t <= r ) or (
s <= t &
t <= q ) )
by Th1, Th2;
then A5:
p < t
by A1, XXREAL_0:2;
t <= q
by A2, A4, XXREAL_0:2;
hence
t in ].p,q.]
by A5, Th2;
verum
end;
assume
t in ].p,q.]
; t in ].p,r.] \/ [.s,q.]
then
( ( p < t & t <= r ) or ( s <= t & t <= q ) )
by A3, Th2, XXREAL_0:2;
then
( t in ].p,r.] or t in [.s,q.] )
by Th1, Th2;
hence
t in ].p,r.] \/ [.s,q.]
by XBOOLE_0:def 3; verum