let X be non empty set ; :: thesis: 1 c= card X
assume not 1 c= card X ; :: thesis: contradiction
then card X in {0} by ORDINAL1:16, CARD_1:49;
hence contradiction by TARSKI:def 1; :: thesis: verum