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