let T be TopSpace; :: thesis: for A being Subset of T holds
( A is perfect iff Der A = A )
let A be Subset of T; :: thesis: ( A is perfect iff Der A = A )
thus ( A is perfect implies Der A = A ) by Lm1; :: thesis: ( Der A = A implies A is perfect )
assume A1: Der A = A ; :: thesis: A is perfect
A2: Cl A = (Der A) \/ A by Th29
.= A by A1 ;
A is dense-in-itself by A1;
hence A is perfect by A2; :: thesis: verum