theorem :: MODCAT_1:5

for R being Ring
for UN being Universe ex x being object st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum } & GO x, TrivialLMod R,R )