ws1s; ex2 X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18: 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) & ((x1 in X8 & x2 in X8) => x1 = x2) & ((x1 in X9 & x2 in X9) => x1 = x2) & ((x1 in X10 & x2 in X10) => x1 = x2) & ((x1 in X11 & x2 in X11) => x1 = x2) & ((x1 in X12 & x2 in X12) => x1 = x2) & ((x1 in X13 & x2 in X13) => x1 = x2) & ((x1 in X14 & x2 in X14) => x1 = x2) & ((x1 in X15 & x2 in X15) => x1 = x2) & ((x1 in X16 & x2 in X16) => x1 = x2) & ((x1 in X17 & x2 in X17) => x1 = x2) & ((x1 in X18 & x2 in X18) => x1 = x2);