TrivialLMod INT.Ring = ModuleStr(# {0},op2,op0,(pr2 ( the carrier of INT.Ring,{0})) #) by MOD_2:def 1;
then the carrier of (TrivialLMod INT.Ring) = {0} ;
hence ( TrivialLMod INT.Ring is trivial & not TrivialLMod INT.Ring is empty & TrivialLMod INT.Ring is strict ) ; :: thesis: verum