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