theorem Th27: :: CARD_1:28

for X being set
for x being object holds
( X,{x} are_equipotent iff ex x being object st X = {x} )