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