:: deftheorem Def15 defines subtraction NOMIN_4:def 15 :
for A being set st A is complex-containing holds
for b₂ being Function of [:A,A:],A holds
( b₂ = subtraction A iff for x, y being object st x in A & y in A holds
b₂ . (x,y) = subtraction (x,y) );