H₁( <NAT,+> ) = NAT by Def27;
hence ( addnat = addreal || NAT & addnat = addint || NAT ) by Th24, GR_CY_1:def 3; :: thesis: verum