let X, x be set ; :: thesis: ( x in X implies (X \ {x}) \/ {x} = X )
assume x in X ; :: thesis: (X \ {x}) \/ {x} = X
then A1: {x} is Subset of X by SUBSET_1:41;
{x} \/ (X \ {x}) = {x} \/ X by XBOOLE_1:39
.= X by A1, XBOOLE_1:12 ;
hence (X \ {x}) \/ {x} = X ; :: thesis: verum