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