let X be finite set ; :: thesis: ( 1 = card X implies ex u being object st X = {u} )
assume 1 = card X ; :: thesis: ex u being object st X = {u}
then card X = card {0} by CARD_1:30;
hence ex u being object st X = {u} by CARD_1:29; :: thesis: verum