:: deftheorem Def16 defines primitive-recursive COMPUT_1:def 16 :
for x being set holds
( x is primitive-recursive iff x in PrimRec );