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