:: deftheorem Def11 defines gcd-like GCD_1:def 11 :
for R being non empty multLoopStr holds
( R is gcd-like iff for x, y being Element of R ex z being Element of R st
( z divides x & z divides y & ( for zz being Element of R st zz divides x & zz divides y holds
zz divides z ) ) );