theorem :: GLIB_003:57
for G being VGraph
for v being Vertex of G
for x being set holds v in (G .labelVertex (v,x)) .labeledV()