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