let T be non empty TopSpace; :: thesis: for A being Subset of T
for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )
let A be Subset of T; :: thesis: for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )
let x be set ; :: thesis: ( x in Der A iff x is_an_accumulation_point_of A )
thus ( x in Der A implies x is_an_accumulation_point_of A ) by Def3; :: thesis: ( x is_an_accumulation_point_of A implies x in Der A )
assume A1: x is_an_accumulation_point_of A ; :: thesis: x in Der A
then x is Point of T by Th17;
hence x in Der A by A1, Def3; :: thesis: verum