let x1, x2 be Point of T; :: thesis: ( S is_convergent_to x1 & S is_convergent_to x2 implies x1 = x2 )
assume that
A3: S is_convergent_to x1 and
A4: S is_convergent_to x2 ; :: thesis: x1 = x2
consider x being Point of T such that
A5: Lim S = {x} by A1;
A6: x2 in {x} by A4, A5, FRECHET:def 5;
x1 in Lim S by A3, FRECHET:def 5;
then x1 = x by A5, TARSKI:def 1;
hence x1 = x2 by A6, TARSKI:def 1; :: thesis: verum