let x be set ; :: thesis: ( x is primitive-recursive implies ( x is Relation-like & x is Function-like ) )
assume x in PrimRec ; :: according to COMPUT_1:def 16 :: thesis: ( x is Relation-like & x is Function-like )
hence ( x is Relation-like & x is Function-like ) ; :: thesis: verum