let X be Subset of (HFuncs NAT); :: thesis: ( X is primitive-recursively_closed implies PrimRec c= X )
set S = { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;
assume X is primitive-recursively_closed ; :: thesis: PrimRec c= X
then A1: X in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimRec or x in X )
assume x in PrimRec ; :: thesis: x in X
hence x in X by A1, SETFAM_1:def 1; :: thesis: verum