let x, X be set ; :: thesis: ( not x in X implies (X \/ {x}) \ {x} = X )
assume not x in X ; :: thesis: (X \/ {x}) \ {x} = X
then ( (X \/ {x}) \ {x} = X \ {x} & X \ {x} = X ) by Th65, XBOOLE_1:40;
hence (X \/ {x}) \ {x} = X ; :: thesis: verum