let U be Universe; :: thesis: not GroupObjects U is U -petit
assume GroupObjects U is U -petit ; :: thesis: contradiction
then consider x being Element of U such that
A1: x, GroupObjects U are_equipotent ;
GroupObjects U,U are_equipotent by Th83;
hence contradiction by A1, CLASSES4:30, WELLORD2:15; :: thesis: verum