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.[ )
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, Th4;
not p in [.s,t.[
by A6, Th3;
hence
p in ].r,t.[ \ [.s,t.[
by A8, XBOOLE_0:def 5; verum