:: deftheorem Def1 defines hcflat NAT_LAT:def 1 :
for b₁ being BinOp of NAT holds
( b₁ = hcflat iff for n, m being Nat holds b₁ . (m,n) = m gcd n );