let X be set ; :: thesis: for c, d being object st ex a, b being object st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d holds
X = {c,d}
let c, d be object ; :: thesis: ( ex a, b being object st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d implies X = {c,d} )
assume that
A1: ex a, b being object st
( a <> b & X = {a,b} ) and
A2: c in X and
A3: d in X and
A4: c <> d ; :: thesis: X = {c,d}
consider a, b being object such that
a <> b and
A5: X = {a,b} by A1;
A6: X c= {c,d}

proof

A7: ( d = a or d = b ) by A3, A5, TARSKI:def 2;
A8: ( c = a or c = b ) by A2, A5, TARSKI:def 2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in {c,d} )
assume A9: x in X ; :: thesis: x in {c,d}

per cases ( x = a or x = b ) by A5, A9, TARSKI:def 2;

suppose x = a ; :: thesis: x in {c,d}

hence x in {c,d} by A4, A8, A7, TARSKI:def 2; :: thesis: verum

end;

suppose x = b ; :: thesis: x in {c,d}

hence x in {c,d} by A4, A8, A7, TARSKI:def 2; :: thesis: verum

end;

end;

end;

{c,d} c= X by A2, A3, ZFMISC_1:32;
hence X = {c,d} by A6; :: thesis: verum