:: deftheorem Def14 defines primitive-recursively_closed COMPUT_1:def 14 :
for X being set holds
( X is primitive-recursively_closed iff ( 0 const 0 in X & 1 succ 1 in X & ( for n, i being Element of NAT st 1 <= i & i <= n holds
n proj i in X ) & X is composition_closed & X is primitive-recursion_closed ) );