let T be non empty homogeneous TopSpace; :: thesis: ( ex p being Point of T st {p} is closed implies T is T_1 )
given p being Point of T such that A1: {p} is closed ; :: thesis: T is T_1

now :: thesis: for q being Point of T holds {q} is closed

let q be Point of T; :: thesis: {q} is closed
consider f being Homeomorphism of T such that
A2: f . p = q by Def6;
dom f = the carrier of T by FUNCT_2:def 1;
then Im (f,p) = {(f . p)} by FUNCT_1:59;
hence {q} is closed by A1, A2, TOPS_2:58; :: thesis: verum

end;

hence T is T_1 by URYSOHN1:19; :: thesis: verum