for k, n being Nat
for a, b being set st card a = n + k & card b = n + k holds
( card (a /\ b) = n iff card (a \/ b) = n + (2 * k) )