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