set G2 = G .set (OrderingSelector,X);
A1:
(G .set (OrderingSelector,X)) . VLabelSelector = G . VLabelSelector
by GLIB_003:def 3, GLIB_000:9;
VLabelSelector in dom G
by GLIB_003:def 6;
then
VLabelSelector in (dom G) \/ {OrderingSelector}
by XBOOLE_0:def 3;
then A2:
VLabelSelector in dom (G .set (OrderingSelector,X))
by GLIB_000:7;
the_Vertices_of G = the_Vertices_of (G .set (OrderingSelector,X))
by Lm1, GLIB_000:10;
then
ex f being Function st
( (G .set (OrderingSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (OrderingSelector,X)) )
by A1, GLIB_003:def 6;
hence
G .set (OrderingSelector,X) is [VLabeled]
by A2, GLIB_003:def 6; verum