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