set G2 = the addVertices of G,V;

set G3 = the addVertices of G,V | _GraphSelectors;

take the addVertices of G,V | _GraphSelectors ; :: thesis: ( the addVertices of G,V | _GraphSelectors is Supergraph of G & the addVertices of G,V | _GraphSelectors is addVertices of G,V & the addVertices of G,V | _GraphSelectors is plain )

thus ( the addVertices of G,V | _GraphSelectors is Supergraph of G & the addVertices of G,V | _GraphSelectors is addVertices of G,V & the addVertices of G,V | _GraphSelectors is plain ) by Th9, GLIB_006:80; :: thesis: verum

set G3 = the addVertices of G,V | _GraphSelectors;

take the addVertices of G,V | _GraphSelectors ; :: thesis: ( the addVertices of G,V | _GraphSelectors is Supergraph of G & the addVertices of G,V | _GraphSelectors is addVertices of G,V & the addVertices of G,V | _GraphSelectors is plain )

thus ( the addVertices of G,V | _GraphSelectors is Supergraph of G & the addVertices of G,V | _GraphSelectors is addVertices of G,V & the addVertices of G,V | _GraphSelectors is plain ) by Th9, GLIB_006:80; :: thesis: verum