theorem :: CARD_1:69

for X being set
for x being object holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )