ws1s;
ex1 x1: ex1 x2: ex1 x3: x1 < x2 & x2 < x3;