let X, x be set ; :: thesis: ( not x in X implies X \ {x} = X )
assume A1: not x in X ; :: thesis: X \ {x} = X

now :: thesis: not X meets {x}

assume X meets {x} ; :: thesis: contradiction
then consider y being object such that
A2: y in X /\ {x} by XBOOLE_0:4;
( y in X & y in {x} ) by A2, XBOOLE_0:def 4;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum

end;

hence X \ {x} = X by XBOOLE_1:83; :: thesis: verum