0 const 0 in PrimRec by Th68;
hence not for b₁ being Element of PrimRec holds b₁ is empty ; :: thesis: verum