set G2 = the addAdjVertex of G,v,e,w;

set G3 = the addAdjVertex of G,v,e,w | _GraphSelectors;

take the addAdjVertex of G,v,e,w | _GraphSelectors ; :: thesis: ( the addAdjVertex of G,v,e,w | _GraphSelectors is Supergraph of G & the addAdjVertex of G,v,e,w | _GraphSelectors is addAdjVertex of G,v,e,w & the addAdjVertex of G,v,e,w | _GraphSelectors is plain )

thus ( the addAdjVertex of G,v,e,w | _GraphSelectors is Supergraph of G & the addAdjVertex of G,v,e,w | _GraphSelectors is addAdjVertex of G,v,e,w & the addAdjVertex of G,v,e,w | _GraphSelectors is plain ) by Th9, GLIB_006:124; :: thesis: verum

set G3 = the addAdjVertex of G,v,e,w | _GraphSelectors;

take the addAdjVertex of G,v,e,w | _GraphSelectors ; :: thesis: ( the addAdjVertex of G,v,e,w | _GraphSelectors is Supergraph of G & the addAdjVertex of G,v,e,w | _GraphSelectors is addAdjVertex of G,v,e,w & the addAdjVertex of G,v,e,w | _GraphSelectors is plain )

thus ( the addAdjVertex of G,v,e,w | _GraphSelectors is Supergraph of G & the addAdjVertex of G,v,e,w | _GraphSelectors is addAdjVertex of G,v,e,w & the addAdjVertex of G,v,e,w | _GraphSelectors is plain ) by Th9, GLIB_006:124; :: thesis: verum