theorem :: GLIB_003:54

for G being _finite VGraph
for v, x being set st v in the_Vertices_of G & not v in G .labeledV() holds
card ((G .labelVertex (v,x)) .labeledV()) = (card (G .labeledV())) + 1