let T be TopSpace; for A being Subset of T st A is closed & A is dense-in-itself holds
Der A = A
let A be Subset of T; ( A is closed & A is dense-in-itself implies Der A = A )
assume A1:
( A is closed & A is dense-in-itself )
; Der A = A
then A =
Cl A
by PRE_TOPC:22
.=
(Der A) \/ A
by Th29
;
hence
Der A c= A
by XBOOLE_1:7; XBOOLE_0:def 10 A c= Der A
thus
A c= Der A
by A1; verum