:: deftheorem Def2 defines recip RINGFRAC:def 6 :
for R being commutative Ring
for r being Element of R st r in Unit_Set R holds
for b₃ being Element of R holds
( b₃ = recip r iff b₃ * r = 1. R );