let G be non empty finite 1-sorted ; :: thesis: card G >= 1
consider g being Element of G;
( {g} c= the carrier of G & card {g} = 1 ) by CARD_1:50, ZFMISC_1:37;
hence card G >= 1 by NAT_1:44; :: thesis: verum