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 )

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

hence
I = {i,j}
by TARSKI:def 2; :: thesis: verum
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

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;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

then
card {x,i,j} c= card I
by CARD_1:11;
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;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

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