:: deftheorem Def8 defines hcflatplus NAT_LAT:def 8 :
for b₁ being BinOp of NATPLUS holds
( b₁ = hcflatplus iff for m, n being NatPlus holds b₁ . (m,n) = m gcd n );