consider x being Element of W, y being Order of x;
RelStr(# x,y #) as_1-sorted = RelStr(# x,y #) by Def1;
hence not POSETS W is empty by Def2; :: thesis: verum