theorem :: FRECHET2:44

for T being non empty TopSpace st T is T_2 holds
T is T_1 by Lm4;