let x, y be object ; :: thesis: for X being set st not x in X & not y in X holds
X = X \ {x,y}
let X be set ; :: thesis: ( not x in X & not y in X implies X = X \ {x,y} )
( X \ {x,y} = X iff X misses {x,y} ) by XBOOLE_1:83;
hence ( not x in X & not y in X implies X = X \ {x,y} ) by Lm20; :: thesis: verum