let T be non empty TopSpace; :: thesis: ( T is T_2 implies T is T_1 )
assume T is T_2 ; :: thesis: T is T_1
then for p being Point of T holds {p} is closed by PCOMPS_1:7;
hence T is T_1 by URYSOHN1:19; :: thesis: verum