theorem :: GLIB_003:39

for G being VGraph
for v, x being set st v in the_Vertices_of G holds
(the_VLabel_of (G .labelVertex (v,x))) . v = x