:: deftheorem defines are_normalized_wrt GCD_1:def 15 :
for R being non empty well-unital associative gcd-like multLoopStr_0
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_normalized_wrt Amp iff ( gcd (x,y,Amp) = 1. R & y in Amp & y <> 0. R ) );