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 Th2, Th3;
then A4:
r < p
by A1, XXREAL_0:2;
p < t
by A2, A3, XXREAL_0:2;
hence
p in ].r,t.[
by A4, Th4;
verum
end;
assume
p in ].r,t.[
; p in ].r,s.] \/ [.s,t.[
then
( ( r < p & p <= s ) or ( s <= p & p < t ) )
by Th4;
then
( p in ].r,s.] or p in [.s,t.[ )
by Th2, Th3;
hence
p in ].r,s.] \/ [.s,t.[
by XBOOLE_0:def 3; verum