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