for K being Ring
for V being LeftMod of K st K is trivial holds
V is trivial by Th5;