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, Th65;
meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } c= HFuncs NAT by A2, SETFAM_1:def 1;
hence meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } is Subset of (HFuncs NAT) ; :: thesis: verum