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:80;
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