consider x being Element of PrimRec ;
take x ; :: thesis: x is primitive-recursive
thus x is primitive-recursive ; :: thesis: verum