let T be non empty TopSpace; :: thesis: for A being Subset of T st T is T_1 & A is dense-in-itself holds
Cl A is dense-in-itself
let A be Subset of T; :: thesis: ( T is T_1 & A is dense-in-itself implies Cl A is dense-in-itself )
assume A1: T is T_1 ; :: thesis: ( not A is dense-in-itself or Cl A is dense-in-itself )
assume A is dense-in-itself ; :: thesis: Cl A is dense-in-itself
then A c= Der A ;
then A2: Der A = A \/ (Der A) by XBOOLE_1:12
.= Cl A by Th29 ;
Der (Cl A) = Der (A \/ (Der A)) by Th29
.= (Der A) \/ (Der (Der A)) by Th31
.= Cl A by A1, A2, Th32, XBOOLE_1:12 ;
hence Cl A is dense-in-itself ; :: thesis: verum