G .set ELabelSelector ,X == G by Lm3;
hence not G .set ELabelSelector ,X is trivial by GLIB_000:92; :: thesis: verum