for X, x being set st card (union X) = 1 holds
X is pairfree