for K being Ring
for V being LeftMod of K holds
( V is trivial iff ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (0). V )