let G be non empty finite 1-sorted ; :: thesis: card G >= 1
set g = the Element of G;
( { the Element of G} c= the carrier of G & card { the Element of G} = 1 ) by CARD_1:30, ZFMISC_1:31;
hence card G >= 1 by NAT_1:43; :: thesis: verum