:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :
for G being VGraph
for v, x being object holds
( ( v in the_Vertices_of G implies G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) ) & ( not v in the_Vertices_of G implies G .labelVertex (v,x) = G ) );