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