:: deftheorem defines +` CARD_2:def 1 :
for M, N being Cardinal holds M +` N = card (M +^ N);