let X, x be set ; :: thesis: ( card X = card {x} iff ex x being set st X = {x} )
( card X = card {x} iff X,{x} are_equipotent ) by Th21;
hence ( card X = card {x} iff ex x being set st X = {x} ) by Th48; :: thesis: verum