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