:: deftheorem Def4 defines / GCD_1:def 4 :
for R being commutative domRing-like Ring
for x, y being Element of R st y divides x & y <> 0. R holds
for b₄ being Element of R holds
( b₄ = x / y iff b₄ * y = x );