G == G .set (OrderingSelector,X) by Th3;
hence not G .set (OrderingSelector,X) is edgeless by GLIB_008:52; :: thesis: verum