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

assume A1: T is T_1 ; :: thesis: T is T_1/2

for A being Subset of T holds Der A is closed

proof

hence
T is T_1/2
; :: thesis: verum
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;Der A = Cl (Der A) by A1, TOPGEN_1:33;

hence Der A is closed ; :: thesis: verum