theorem Th19: :: GLIB_013:19
for G1, G2 being _Graph
for c being Cardinal st the_Edges_of G1 = the_Edges_of G2 & G1 is c -edge holds
G2 is c -edge ;