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