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 }