theorem :: FRECHET2:45

for T being non empty TopSpace st not T is T_1 holds
ex x1, x2 being Point of T ex S being sequence of T st
( S = NAT --> x1 & x1 <> x2 & S is_convergent_to x2 ) by Lm3;