for G being EVGraph
for v, x being set holds the_ELabel_of G = the_ELabel_of (G .labelVertex (v,x))