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