:: deftheorem Def3 defines opp ARYTM_0:def 3 :
for x, b₂ being Element of REAL holds
( b₂ = opp x iff + (x,b₂) = 0 );