let T be non empty TopSpace; :: thesis: for A being Subset of T holds Der A = { x where x is Point of T : x in Cl (A \ {x}) }
let A be Subset of T; :: thesis: Der A = { x where x is Point of T : x in Cl (A \ {x}) }
thus Der A c= { x where x is Point of T : x in Cl (A \ {x}) } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Point of T : x in Cl (A \ {x}) } c= Der A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Der A or x in { x where x is Point of T : x in Cl (A \ {x}) } )
assume x in Der A ; :: thesis: x in { x where x is Point of T : x in Cl (A \ {x}) }
then x is_an_accumulation_point_of A by TOPGEN_1:def 3;
then x in Cl (A \ {x}) by TOPGEN_1:def 2;
hence x in { x where x is Point of T : x in Cl (A \ {x}) } ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Point of T : x in Cl (A \ {x}) } or y in Der A )
assume y in { x where x is Point of T : x in Cl (A \ {x}) } ; :: thesis: y in Der A
then consider z being Point of T such that
A1: z = y and
A2: z in Cl (A \ {z}) ;
z is_an_accumulation_point_of A by A2, TOPGEN_1:def 2;
hence y in Der A by A1, TOPGEN_1:def 3; :: thesis: verum