let x be object ; :: thesis: for X being set st not x in X holds
(X \/ {x}) \ {x} = X
let 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, Th56; :: thesis: verum