theorem Th83: :: CLASSES5:81

for U being Universe holds GroupObjects U,U are_equipotent