let G2, G3 be _Graph; :: thesis: for V being set
for G1 being addVertices of G2,V st G2 == G3 holds
G1 is addVertices of G3,V
let V be set ; :: thesis: for G1 being addVertices of G2,V st G2 == G3 holds
G1 is addVertices of G3,V
let G1 be addVertices of G2,V; :: thesis: ( G2 == G3 implies G1 is addVertices of G3,V )
assume A1: G2 == G3 ; :: thesis: G1 is addVertices of G3,V
then ( the_Vertices_of G3 = the_Vertices_of G2 & the_Edges_of G3 = the_Edges_of G2 & the_Target_of G3 = the_Target_of G2 & the_Source_of G3 = the_Source_of G2 ) by GLIB_000:def 34;
then A2: ( the_Vertices_of G1 = (the_Vertices_of G3) \/ V & the_Edges_of G1 = the_Edges_of G3 & the_Source_of G1 = the_Source_of G3 & the_Target_of G1 = the_Target_of G3 ) by GLIB_006:def 10;
G2 is Supergraph of G3 by A1, GLIB_006:58;
then G1 is Supergraph of G3 by GLIB_006:62;
hence G1 is addVertices of G3,V by A2, GLIB_006:def 10; :: thesis: verum