G .set (ELabelSelector,X) == G by Lm3;
hence G .set (ELabelSelector,X) is finite by GLIB_000:92; :: thesis: verum