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