ws1s; ex2 X1: all1 x: ex1 y, z: ~(( (x in X1 & x <= y & y <= z & z in X1) => y in X1 ));