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