let X, Y, x be set ; :: thesis: ( not x in X implies X \ (Y \/ {x}) = X \ Y )
assume not x in X ; :: thesis: X \ (Y \/ {x}) = X \ Y
then A1: not x in X \ Y ;
thus X \ (Y \/ {x}) = (X \ Y) \ {x} by XBOOLE_1:41
.= X \ Y by A1, ZFMISC_1:57 ; :: thesis: verum