:: deftheorem defines unital GCD_1:def 2 :
for R being non empty multLoopStr
for x being Element of R holds
( x is unital iff x divides 1. R );