let x, y, 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 Lm21; :: thesis: verum