let r, s, t be ExtReal; :: thesis: ( r <= s & s < t implies [.r,s.] /\ [.s,t.[ = {s} )
assume that
A1: r <= s and
A2: s < t ; :: thesis: [.r,s.] /\ [.s,t.[ = {s}

now :: thesis: 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 ; :: thesis: ( ( x in [.r,s.] /\ [.s,t.[ implies x = s ) & ( x = s implies x in [.r,s.] /\ [.s,t.[ ) )

hereby :: thesis: ( x = s implies x in [.r,s.] /\ [.s,t.[ )

assume A3: x in [.r,s.] /\ [.s,t.[ ; :: thesis: x = s
then reconsider p = x as ExtReal ;
A4: p in [.r,s.] by A3, XBOOLE_0:def 4;
p in [.s,t.[ by A3, XBOOLE_0:def 4;
then A5: s <= p by Th3;
p <= s by A4, Th1;
hence x = s by A5, XXREAL_0:1; :: thesis: verum

end;

assume A6: x = s ; :: thesis: 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; :: thesis: verum

end;

hence [.r,s.] /\ [.s,t.[ = {s} by TARSKI:def 1; :: thesis: verum