set D = {(TrivialLMod R)};
take {(TrivialLMod R)} ; :: thesis: for x being Element of {(TrivialLMod R)} holds x is strict LeftMod of strict
thus for x being Element of {(TrivialLMod R)} holds x is strict LeftMod of strict by TARSKI:def 1; :: thesis: verum