:: deftheorem defines trivial LMOD_6:def 1 :
for K being Ring holds
( K is trivial iff 0. K = 1_ K );