let x, X be set ; :: thesis: ( x in X iff X = (X \ {x}) \/ {x} )
( x in X iff {x} c= X ) by ZFMISC_1:37;
hence ( x in X iff X = (X \ {x}) \/ {x} ) by XBOOLE_1:7, XBOOLE_1:45; :: thesis: verum