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

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