theorem :: FRECHET2:7

for T being non empty TopSpace st T is first-countable holds
( T is T_2 iff 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 )