theorem :: CARD_1:42

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