theorem :: CLASSES5:82

for U being Universe holds not GroupObjects U is U -petit