let G be _Graph; :: thesis: for V being set
for G1, G2 being addVertices of G,V holds G1 == G2
let V be set ; :: thesis: for G1, G2 being addVertices of G,V holds G1 == G2
let G1, G2 be addVertices of G,V; :: thesis: G1 == G2
( the_Vertices_of G1 = (the_Vertices_of G) \/ V & the_Edges_of G1 = the_Edges_of G & the_Source_of G1 = the_Source_of G & the_Target_of G1 = the_Target_of G & 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;
hence G1 == G2 by GLIB_000:def 34; :: thesis: verum