set G0 = G .set (OrderingSelector,X);
G . VLabelSelector = (G .set (OrderingSelector,X)) . VLabelSelector by GLIB_000:9, GLIB_003:def 3;
then the_VLabel_of G = (G .set (OrderingSelector,X)) . VLabelSelector by GLIB_003:def 9;
hence G .set (OrderingSelector,X) is vlabel-distinct by GLIB_003:def 9; :: thesis: verum