:: deftheorem Def6 defines Der TOPGEN_1:def 6 :
for T being TopSpace
for F, b₃ being Subset-Family of T holds
( b₃ = Der F iff for A being Subset of T holds
( A in b₃ iff ex B being Subset of T st
( A = Der B & B in F ) ) );