:: deftheorem Def4 defines inv ARYTM_0:def 4 :
for x, b₂ being Element of REAL holds
( ( x <> 0 implies ( b₂ = inv x iff * (x,b₂) = 1 ) ) & ( not x <> 0 implies ( b₂ = inv x iff b₂ = 0 ) ) );