let T be non empty TopSpace; :: thesis: ( T is T_1 implies for p being Point of T holds Cl {p} = {p} )
assume A1: T is T_1 ; :: thesis: for p being Point of T holds Cl {p} = {p}
let p be Point of T; :: thesis: Cl {p} = {p}
{p} is closed by A1, URYSOHN1:19;
then A2: Cl {p} c= {p} by TOPS_1:5;
{p} c= Cl {p} by PRE_TOPC:18;
hence Cl {p} = {p} by A2, XBOOLE_0:def 10; :: thesis: verum