let T be non empty TopSpace; :: thesis: for A being Subset of
for x being set holds
( x in Der A iff x is_an_accumulation_point_of A )
let A be Subset of ; :: 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 by Th17;
hence x in Der A by A1, Def3; :: thesis: verum