let T be non empty TopSpace; :: thesis: ( ( for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ) implies T is T_1 )
assume A1: for S being sequence of T
for x1, x2 being Point of T st x1 in Lim S & x2 in Lim S holds
x1 = x2 ; :: thesis: T is T_1
assume not T is T_1 ; :: thesis: contradiction
then consider x1, x2 being Point of T, S being sequence of T such that
A2: S = NAT --> x1 and
A3: x1 <> x2 and
A4: S is_convergent_to x2 by Lm3;
S is_convergent_to x1 by A2, FRECHET:22;
then A5: x1 in Lim S by FRECHET:def 5;
x2 in Lim S by A4, FRECHET:def 5;
hence contradiction by A1, A3, A5; :: thesis: verum