theorem Th7: :: TOPS_2:7

for T being set
for F being Subset-Family of T st F <> {} holds
union (COMPLEMENT F) = (meet F) `