let I be 2 -element set ; :: thesis: for i, j being Element of I st i <> j holds
I = {i,j}
let i, j be Element of I; :: thesis: ( i <> j implies I = {i,j} )
assume A1: i <> j ; :: thesis: I = {i,j}
for x being object holds
( ( x = i or x = j ) iff x in I )
proof
let x be object ; :: thesis: ( ( x = i or x = j ) iff x in I )
thus ( ( x = i or x = j ) implies x in I ) ; :: thesis: ( not x in I or x = i or x = j )
assume A2: x in I ; :: thesis: ( x = i or x = j )
assume ( x <> i & x <> j ) ; :: thesis: contradiction
then A3: card {x,i,j} = 3 by A1, CARD_2:58;
{x,i,j} c= I
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,i,j} or z in I )
assume z in {x,i,j} ; :: thesis: z in I
then ( z = x or z = i or z = j ) by ENUMSET1:def 1;
hence z in I by A2; :: thesis: verum
end;
then card {x,i,j} c= card I by CARD_1:11;
then A4: {0,1,2} c= 2 by A3, CARD_1:def 7, CARD_1:51;
2 in {0,1,2} by ENUMSET1:def 1;
then 2 in 2 by A4;
hence contradiction ; :: thesis: verum
end;
hence I = {i,j} by TARSKI:def 2; :: thesis: verum