let x be Relation; :: thesis: ( x is primitive-recursive implies ( x is homogeneous & x is to-naturals & x is NAT * -defined ) )
assume x in PrimRec ; :: according to COMPUT_1:def 16 :: thesis: ( x is homogeneous & x is to-naturals & x is NAT * -defined )
hence ( x is homogeneous & x is to-naturals & x is NAT * -defined ) ; :: thesis: verum