theorem Th25: :: CARD_1:26

for X being set st X, {} are_equipotent holds
X = {} by RELAT_1:42;