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 } ;
( HFuncs NAT in {(HFuncs NAT )} & {(HFuncs NAT )} c= bool (HFuncs NAT ) ) by TARSKI:def 1, ZFMISC_1:80;
then A1: HFuncs NAT in { R where R is Subset of (HFuncs NAT ) : R is primitive-recursively_closed } by 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 A1, 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