:: deftheorem Def3 defines Der TOPGEN_1:def 3 :
for T being TopStruct
for A, b₃ being Subset of T holds
( b₃ = Der A iff for x being set st x in the carrier of T holds
( x in b₃ iff x is_an_accumulation_point_of A ) );