1 succ 1 in PrimRec by Th70;
hence 1 succ 1 is primitive-recursive ; :: thesis: verum