set G2 = the addEdge of G,v,e,w;
set G3 = the addEdge of G,v,e,w | _GraphSelectors;
take the addEdge of G,v,e,w | _GraphSelectors ; :: thesis: ( the addEdge of G,v,e,w | _GraphSelectors is Supergraph of G & the addEdge of G,v,e,w | _GraphSelectors is addEdge of G,v,e,w & the addEdge of G,v,e,w | _GraphSelectors is plain )
thus ( the addEdge of G,v,e,w | _GraphSelectors is Supergraph of G & the addEdge of G,v,e,w | _GraphSelectors is addEdge of G,v,e,w & the addEdge of G,v,e,w | _GraphSelectors is plain ) by GLIB_000:128, GLIB_006:101; :: thesis: verum