theorem :: TOPGEN_1:24

for T being non empty TopSpace
for F being Subset-Family of T st F = {} holds
Der F = {}