let T be non empty TopSpace; :: thesis: for A being Subset of T holds
( A is closed iff Der A c= A )
let A be Subset of T; :: thesis: ( A is closed iff Der A c= A )

hereby :: thesis: ( Der A c= A implies A is closed )

assume A is closed ; :: thesis: Der A c= A
then A1: A = Cl A by PRE_TOPC:22;
Cl A = A \/ (Der A) by TOPGEN_1:29;
hence Der A c= A by A1, XBOOLE_1:7; :: thesis: verum

end;

assume A2: Der A c= A ; :: thesis: A is closed
Cl A = A \/ (Der A) by TOPGEN_1:29
.= A by A2, XBOOLE_1:12 ;
hence A is closed ; :: thesis: verum