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 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;
per cases ( x1 = a or x1 = b or x1 = c or x1 = d ) by A3, 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, A4, 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, A4, 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, A4, 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, A4, ENUMSET1:def 2; :: thesis: verum
end;
end;
end;
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} )
assume A5: 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 A5, ENUMSET1:def 2;
suppose A6: 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 A6, RELAT_1:def 10; :: thesis: verum
end;
suppose A7: 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 A7, RELAT_1:def 10; :: thesis: verum
end;
suppose A8: 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 A8, RELAT_1:def 10; :: thesis: verum
end;
suppose A9: 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 A9, RELAT_1:def 10; :: thesis: verum
end;
end;