ws1s; ex2 X1, X2, X3, X4, X5, X6, X7: all1 x1, x2: ((x1 in X1 & x2 in X1) => x1 = x2) & ((x1 in X2 & x2 in X2) => x1 = x2) & ((x1 in X3 & x2 in X3) => x1 = x2) & ((x1 in X4 & x2 in X4) => x1 = x2) & ((x1 in X5 & x2 in X5) => x1 = x2) & ((x1 in X6 & x2 in X6) => x1 = x2) & ((x1 in X7 & x2 in X7) => x1 = x2);