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}

assume A5: x in {[a,a],[b,b],[c,c],[d,d]} ; :: thesis: x in id {a,b,c,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 object ; :: 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} )
let x be object ; :: 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 object such that

A2: x = [x1,y1] and

A3: x1 in {a,b,c,d} and

y1 in {a,b,c,d} by RELSET_1:2;

A4: x1 = y1 by A1, A2, RELAT_1:def 10;

end;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 object such that

A2: x = [x1,y1] and

A3: x1 in {a,b,c,d} and

y1 in {a,b,c,d} by RELSET_1:2;

A4: x1 = y1 by A1, A2, RELAT_1:def 10;

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