theorem :: GLIB_003:43

for G being VGraph
for v1, v2, x being set st v1 <> v2 holds
(the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2