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:10;
hence T is T_1 by URYSOHN1:27; :: thesis: verum