theorem :: GLIB_003:53

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