theorem :: CLASSES5:51

for U being Universe
for G being Group st G is U -element holds
the multF of G is Element of U