theorem :: CARD_2:89

for n being Nat holds
( omega *` (card n) c= omega & (card n) *` omega c= omega )