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