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

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

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 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 )
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;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

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