for m, n being Nat holds
( card n in card m iff n in m ) ;