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