ws1s; ex2 X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20: all1 x: ex1 y, z: ~(( (x in X1 & x <= y & y <= z & z in X1) => y in X1 ) & ( (x in X2 & x <= y & y <= z & z in X2) => y in X2 ) & ( (x in X3 & x <= y & y <= z & z in X3) => y in X3 ) & ( (x in X4 & x <= y & y <= z & z in X4) => y in X4 ) & ( (x in X5 & x <= y & y <= z & z in X5) => y in X5 ) & ( (x in X6 & x <= y & y <= z & z in X6) => y in X6 ) & ( (x in X7 & x <= y & y <= z & z in X7) => y in X7 ) & ( (x in X8 & x <= y & y <= z & z in X8) => y in X8 ) & ( (x in X9 & x <= y & y <= z & z in X9) => y in X9 ) & ( (x in X10 & x <= y & y <= z & z in X10) => y in X10 ) & ( (x in X11 & x <= y & y <= z & z in X11) => y in X11 ) & ( (x in X12 & x <= y & y <= z & z in X12) => y in X12 ) & ( (x in X13 & x <= y & y <= z & z in X13) => y in X13 ) & ( (x in X14 & x <= y & y <= z & z in X14) => y in X14 ) & ( (x in X15 & x <= y & y <= z & z in X15) => y in X15 ) & ( (x in X16 & x <= y & y <= z & z in X16) => y in X16 ) & ( (x in X17 & x <= y & y <= z & z in X17) => y in X17 ) & ( (x in X18 & x <= y & y <= z & z in X18) => y in X18 ) & ( (x in X19 & x <= y & y <= z & z in X19) => y in X19 ) & ( (x in X20 & x <= y & y <= z & z in X20) => y in X20 ));