let E be non empty finite set ; :: thesis: 0 < card E
consider x being Element of E;
card {x} <= card E by NAT_1:44;
hence 0 < card E by CARD_1:50; :: thesis: verum