set x = the Element of PrimRec ;
take the Element of PrimRec ; :: thesis: the Element of PrimRec is primitive-recursive
thus the Element of PrimRec is primitive-recursive ; :: thesis: verum