ws1s; ex2 X1, X2: all1 x1, x2: ((x1 in X1 & x2 in X1) => x1 = x2) & ((x1 in X2 & x2 in X2) => x1 = x2);