let X be set ; :: thesis: ( card X = 1 iff ex x being object st X = {x} )
card {0} = 1 by CARD_1:30;
hence ( card X = 1 implies ex x being object st X = {x} ) by CARD_1:29; :: thesis: ( ex x being object st X = {x} implies card X = 1 )
given x being object such that A1: X = {x} ; :: thesis: card X = 1
thus card X = 1 by A1, CARD_1:30; :: thesis: verum