theorem :: NECKLA_3:2
for a, b, c, d being set holds id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}