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