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, WELLORD2:15, CLASSES4:30; :: thesis: verum