1 = succ 0 ;
then {x},1 are_equipotent by Th28;
hence card {x} = 1 by Def2; :: according to CARD_1:def 7 :: thesis: verum