:: deftheorem Def14 defines subtraction NOMIN_4:def 14 :
for x, y being object st x is Complex & y is Complex holds
for b₃ being Complex holds
( b₃ = subtraction (x,y) iff ex x1, y1 being Complex st
( x1 = x & y1 = y & b₃ = x1 - y1 ) );