let UN be Universe; :: thesis: for R being Ring holds TrivialLMod R in LModObjects UN,R
let R be Ring; :: thesis: TrivialLMod R in LModObjects UN,R
ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,1:],1 : verum } & GO x, TrivialLMod R,R ) by Th7;
hence TrivialLMod R in LModObjects UN,R by Def6; :: thesis: verum