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, Th2;
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, Th2;
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