set G2 = the addAdjVertexAll of G,v,V;

set G3 = the addAdjVertexAll of G,v,V | _GraphSelectors;

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

thus ( the addAdjVertexAll of G,v,V | _GraphSelectors is Supergraph of G & the addAdjVertexAll of G,v,V | _GraphSelectors is addAdjVertexAll of G,v,V & the addAdjVertexAll of G,v,V | _GraphSelectors is plain ) by Th9, GLIB_007:48; :: thesis: verum

set G3 = the addAdjVertexAll of G,v,V | _GraphSelectors;

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

thus ( the addAdjVertexAll of G,v,V | _GraphSelectors is Supergraph of G & the addAdjVertexAll of G,v,V | _GraphSelectors is addAdjVertexAll of G,v,V & the addAdjVertexAll of G,v,V | _GraphSelectors is plain ) by Th9, GLIB_007:48; :: thesis: verum