G == G .set (OrderingSelector,X) by Th3;
hence G .set (OrderingSelector,X) is loopless by GLIB_000:89; :: thesis: verum