set G2 = the addAdjVertexToAll of G,v,V;
set G3 = the addAdjVertexToAll of G,v,V | _GraphSelectors;
reconsider G3 = the addAdjVertexToAll of G,v,V | _GraphSelectors as addAdjVertexToAll of G,v,V by Th9, GLIB_007:30;
take G3 ; :: thesis: G3 is plain
thus G3 is plain ; :: thesis: verum