take TrivialLMod INT.Ring ; :: thesis: TrivialLMod INT.Ring is strict
thus TrivialLMod INT.Ring is strict ; :: thesis: verum