theorem Th1: :: COMBGRAS:1

for n being Nat
for a, b being set st a <> b & card a = n & card b = n holds
( card (a /\ b) in n & n + 1 c= card (a \/ b) )