2 proj 2 in PrimRec by Def17;
hence 2 proj 2 is primitive-recursive ; :: thesis: verum