let r, s, t be ExtReal; ( r <= s & s < t implies [.r,s.] /\ [.s,t.[ = {s} )
assume that
A1:
r <= s
and
A2:
s < t
; [.r,s.] /\ [.s,t.[ = {s}
now for x being object holds
( ( x in [.r,s.] /\ [.s,t.[ implies x = s ) & ( x = s implies x in [.r,s.] /\ [.s,t.[ ) )let x be
object ;
( ( x in [.r,s.] /\ [.s,t.[ implies x = s ) & ( x = s implies x in [.r,s.] /\ [.s,t.[ ) )assume A6:
x = s
;
x in [.r,s.] /\ [.s,t.[A7:
s in [.r,s.]
by A1, Th1;
s in [.s,t.[
by A2, Th3;
hence
x in [.r,s.] /\ [.s,t.[
by A6, A7, XBOOLE_0:def 4;
verum end;
hence
[.r,s.] /\ [.s,t.[ = {s}
by TARSKI:def 1; verum