set G0 = G .set (OrderingSelector,X);

G . ELabelSelector = (G .set (OrderingSelector,X)) . ELabelSelector by GLIB_000:9, GLIB_003:def 2;

then the_ELabel_of G = (G .set (OrderingSelector,X)) . ELabelSelector by GLIB_003:def 8;

hence G .set (OrderingSelector,X) is elabel-distinct by GLIB_003:def 8; :: thesis: verum

G . ELabelSelector = (G .set (OrderingSelector,X)) . ELabelSelector by GLIB_000:9, GLIB_003:def 2;

then the_ELabel_of G = (G .set (OrderingSelector,X)) . ELabelSelector by GLIB_003:def 8;

hence G .set (OrderingSelector,X) is elabel-distinct by GLIB_003:def 8; :: thesis: verum