let x, y be object ; :: thesis: for X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )
let X be set ; :: thesis: ( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) )
thus ( {x,y} \ X = {x} implies ( not x in X & ( y in X or x = y ) ) ) :: thesis: ( not x in X & ( y in X or x = y ) implies {x,y} \ X = {x} )

proof

assume A1: {x,y} \ X = {x} ; :: thesis: ( not x in X & ( y in X or x = y ) )
then x in {x,y} \ X by TARSKI:def 1;
hence not x in X by XBOOLE_0:def 5; :: thesis: ( y in X or x = y )
A2: y in {x,y} by TARSKI:def 2;
assume not y in X ; :: thesis: x = y
then y in {x} by A1, A2, XBOOLE_0:def 5;
hence x = y by TARSKI:def 1; :: thesis: verum

end;

assume A3: ( not x in X & ( y in X or x = y ) ) ; :: thesis: {x,y} \ X = {x}
for z being object holds
( z in {x,y} \ X iff z = x )

proof

let z be object ; :: thesis: ( z in {x,y} \ X iff z = x )
( z in {x,y} \ X iff ( z in {x,y} & not z in X ) ) by XBOOLE_0:def 5;
hence ( z in {x,y} \ X iff z = x ) by A3, TARSKI:def 2; :: thesis: verum

end;

hence {x,y} \ X = {x} by TARSKI:def 1; :: thesis: verum