theorem :: GLIB_003:55

for G being VGraph
for v1, v2, x being set st not v2 in G .labeledV() & v2 in (G .labelVertex (v1,x)) .labeledV() holds
( v1 = v2 & v1 in the_Vertices_of G )