theorem Th3: :: YELLOW_9:3

for T being 1-sorted
for F being Subset-Family of T holds COMPLEMENT F = { (a `) where a is Subset of T : a in F }