let G2, G3 be _Graph; 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 ; for G1 being addVertices of G2,V st G2 == G3 holds
G1 is addVertices of G3,V
let G1 be addVertices of G2,V; ( G2 == G3 implies G1 is addVertices of G3,V )
assume A1:
G2 == G3
; 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; verum