ws1s;
ex2 X: all1 x1, x2, x3: ((x1 in X => x2 in X) & (x2 in X => x3 in X));