theorem Th8: :: TEX_4:8

for Y being non empty TopStruct
for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds
union F is anti-discrete