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