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