let A, x, y be set ; :: thesis: ( A c= {x,y} & x in A & not y in A implies A = {x} )
assume that
A1: A c= {x,y} and
A2: x in A and
A3: not y in A ; :: thesis: A = {x}
per cases ( A = {} or A = {x} or A = {y} or A = {x,y} ) by A1, ZFMISC_1:36;
suppose A = {} ; :: thesis: A = {x}
hence A = {x} by A2; :: thesis: verum
end;
suppose A = {x} ; :: thesis: A = {x}
hence A = {x} ; :: thesis: verum
end;
suppose A = {y} ; :: thesis: A = {x}
hence A = {x} by A3, TARSKI:def 1; :: thesis: verum
end;
suppose A = {x,y} ; :: thesis: A = {x}
hence A = {x} by A3, TARSKI:def 2; :: thesis: verum
end;
end;