ws1s; ex2 X: all2 X1, X2, X3, X4, X5, X6, X7, X8, X9, X10: ( (X1 sub X & X1 sub X2 & X1 ~= X2) => X2 sub X) & ( (X2 sub X & X2 sub X3 & X2 ~= X3) => X3 sub X) & ( (X3 sub X & X3 sub X4 & X3 ~= X4) => X4 sub X) & ( (X4 sub X & X4 sub X5 & X4 ~= X5) => X5 sub X) & ( (X5 sub X & X5 sub X6 & X5 ~= X6) => X6 sub X) & ( (X6 sub X & X6 sub X7 & X6 ~= X7) => X7 sub X) & ( (X7 sub X & X7 sub X8 & X7 ~= X8) => X8 sub X) & ( (X8 sub X & X8 sub X9 & X8 ~= X9) => X9 sub X) & ( (X9 sub X & X9 sub X10 & X9 ~= X10) => X10 sub X);