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