let a, b, c, d be set ; :: thesis: id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}
set X = {a,b,c,d};
thus id {a,b,c,d} c= {[a,a],[b,b],[c,c],[d,d]} :: according to XBOOLE_0:def 10 :: thesis: {[a,a],[b,b],[c,c],[d,d]} c= id {a,b,c,d}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in id {a,b,c,d} or x in {[a,a],[b,b],[c,c],[d,d]} )
assume A1: x in id {a,b,c,d} ; :: thesis: x in {[a,a],[b,b],[c,c],[d,d]}
then consider x1, y1 being set such that
A2: ( x = [x1,y1] & x1 in {a,b,c,d} & y1 in {a,b,c,d} ) by RELSET_1:6;
A3: x1 = y1 by A1, A2, RELAT_1:def 10;

per cases ( x1 = a or x1 = b or x1 = c or x1 = d ) by A2, ENUMSET1:def 2;

suppose x1 = a ; :: thesis: x in {[a,a],[b,b],[c,c],[d,d]}

hence x in {[a,a],[b,b],[c,c],[d,d]} by A2, A3, ENUMSET1:def 2; :: thesis: verum

end;

suppose x1 = b ; :: thesis: x in {[a,a],[b,b],[c,c],[d,d]}

hence x in {[a,a],[b,b],[c,c],[d,d]} by A2, A3, ENUMSET1:def 2; :: thesis: verum

end;

suppose x1 = c ; :: thesis: x in {[a,a],[b,b],[c,c],[d,d]}

hence x in {[a,a],[b,b],[c,c],[d,d]} by A2, A3, ENUMSET1:def 2; :: thesis: verum

end;

suppose x1 = d ; :: thesis: x in {[a,a],[b,b],[c,c],[d,d]}

hence x in {[a,a],[b,b],[c,c],[d,d]} by A2, A3, ENUMSET1:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[a,a],[b,b],[c,c],[d,d]} or x in id {a,b,c,d} )
assume A4: x in {[a,a],[b,b],[c,c],[d,d]} ; :: thesis: x in id {a,b,c,d}

per cases ( x = [a,a] or x = [b,b] or x = [c,c] or x = [d,d] ) by A4, ENUMSET1:def 2;

suppose A5: x = [a,a] ; :: thesis: x in id {a,b,c,d}

a in {a,b,c,d} by ENUMSET1:def 2;
hence x in id {a,b,c,d} by A5, RELAT_1:def 10; :: thesis: verum

end;

suppose A6: x = [b,b] ; :: thesis: x in id {a,b,c,d}

b in {a,b,c,d} by ENUMSET1:def 2;
hence x in id {a,b,c,d} by A6, RELAT_1:def 10; :: thesis: verum

end;

suppose A7: x = [c,c] ; :: thesis: x in id {a,b,c,d}

c in {a,b,c,d} by ENUMSET1:def 2;
hence x in id {a,b,c,d} by A7, RELAT_1:def 10; :: thesis: verum

end;

suppose A8: x = [d,d] ; :: thesis: x in id {a,b,c,d}

d in {a,b,c,d} by ENUMSET1:def 2;
hence x in id {a,b,c,d} by A8, RELAT_1:def 10; :: thesis: verum

end;

end;