theorem Th16: :: TOPGEN_1:16

for T being non empty TopSpace
for A being Subset of T
for x being object holds
( x in Der A iff x is_an_accumulation_point_of A ) by Def3;