consider x being Point of T such that
A2: Lim S = {x} by A1;
take x ; :: thesis: S is_convergent_to x
x in {x} by TARSKI:def 1;
hence S is_convergent_to x by A2, FRECHET:def 5; :: thesis: verum