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