theorem :: TOPGEN_1:4

for T being TopSpace
for F being Subset-Family of T st F = {} holds
Fr F = {}