set G2 = the addAdjVertexFromAll of G,v,V;
set G3 = the addAdjVertexFromAll of G,v,V | _GraphSelectors;
reconsider G3 = the addAdjVertexFromAll of G,v,V | _GraphSelectors as addAdjVertexFromAll of G,v,V by GLIB_000:128, GLIB_007:31;
take G3 ; :: thesis: G3 is plain
thus G3 is plain ; :: thesis: verum