set S = { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;
set T = meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;
A1: {(HFuncs NAT)} c= bool (HFuncs NAT) by ZFMISC_1:68;
HFuncs NAT in {(HFuncs NAT)} by TARSKI:def 1;
then A2: HFuncs NAT in { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } by A1, Th70;
meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } c= HFuncs NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } or x in HFuncs NAT )
assume x in meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ; :: thesis: x in HFuncs NAT
hence x in HFuncs NAT by A2, SETFAM_1:def 1; :: thesis: verum

end;

hence meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } is Subset of (HFuncs NAT) ; :: thesis: verum