G == G .set (ELabelSelector,X) by GLIB_003:7;
hence not G .set (ELabelSelector,X) is acyclic by GLIB_002:44; :: thesis: verum