:: deftheorem Def23 defines addnat BINOP_2:def 23 :
for b₁ being BinOp of NAT holds
( b₁ = addnat iff for n1, n2 being Nat holds b₁ . (n1,n2) = n1 + n2 );