:: deftheorem Def5 defines - XCMPLX_0:def 5 :
for z, b₂ being Complex holds
( b₂ = - z iff z + b₂ = 0 );