HFuncs NAT c= HFuncs NAT ;
then reconsider X = HFuncs NAT as non empty Subset of (HFuncs NAT) ;
take X ; :: thesis: ( X is primitive-recursively_closed & not X is empty )
thus ( X is primitive-recursively_closed & not X is empty ) by Th65; :: thesis: verum