let T be non empty TopSpace; :: thesis: for A being Subset of T holds A ^0 c= Der A

let A be Subset of T; :: thesis: A ^0 c= Der A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^0 or x in Der A )

assume A1: x in A ^0 ; :: thesis: x in Der A

then reconsider p = x as Point of T ;

p is_a_condensation_point_of A by A1, Def10;

then p is_an_accumulation_point_of A by Th49;

hence x in Der A by TOPGEN_1:16; :: thesis: verum

let A be Subset of T; :: thesis: A ^0 c= Der A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^0 or x in Der A )

assume A1: x in A ^0 ; :: thesis: x in Der A

then reconsider p = x as Point of T ;

p is_a_condensation_point_of A by A1, Def10;

then p is_an_accumulation_point_of A by Th49;

hence x in Der A by TOPGEN_1:16; :: thesis: verum