for G1, G2 being VGraph st the_VLabel_of G1 = the_VLabel_of G2 holds
G1 .labeledV() = G2 .labeledV() ;