let E be non empty finite set ; :: thesis: 0 < card E
card { the Element of E} <= card E by NAT_1:43;
hence 0 < card E by CARD_1:30; :: thesis: verum