theorem Th18: :: GLIB_013:18

for G1, G2 being _Graph
for c being Cardinal st the_Vertices_of G1 = the_Vertices_of G2 & G1 is c -vertex holds
G2 is c -vertex ;