let T be non empty TopSpace; :: thesis: ( ( for p being Point of T holds Cl {p} = {p} ) implies T is T_1 )
assume A1: for p being Point of T holds Cl {p} = {p} ; :: thesis: T is T_1
for p being Point of T holds {p} is closed
proof
let p be Point of T; :: thesis: {p} is closed
Cl {p} = {p} by A1;
hence {p} is closed by PRE_TOPC:22; :: thesis: verum
end;
hence T is T_1 by URYSOHN1:19; :: thesis: verum