let r, s, t be ext-real number ; :: 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

let x be set ; :: 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 ext-real number ;
( p in [.r,s.] & p in [.s,t.] ) by A3, XBOOLE_0:def 4;
then ( s <= p & p <= s ) by Th1;
hence x = s by XXREAL_0:1; :: thesis: verum

end;

assume A4: x = s ; :: thesis: x in [.r,s.] /\ [.s,t.]
( s in [.r,s.] & s in [.s,t.] ) by A1, A2, Th1;
hence x in [.r,s.] /\ [.s,t.] by A4, XBOOLE_0:def 4; :: thesis: verum

end;

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