let T be TopSpace; :: thesis: ( T is T_1 implies T is T_1/2 )
assume A1: T is T_1 ; :: thesis: T is T_1/2
for A being Subset of T holds Der A is closed
proof
let A be Subset of T; :: thesis: Der A is closed
Der A = Cl (Der A) by A1, TOPGEN_1:33;
hence Der A is closed ; :: thesis: verum
end;
hence T is T_1/2 ; :: thesis: verum