:: deftheorem defines multiplicative GCD_1:def 10 :
for R being non empty well-unital associative multLoopStr
for Amp being AmpleSet of R holds
( Amp is multiplicative iff for x, y being Element of Amp holds x * y in Amp );