set G2 = the removeVertices of G,V;
set G3 = the removeVertices of G,V | _GraphSelectors;
take the removeVertices of G,V | _GraphSelectors ; :: thesis: ( the removeVertices of G,V | _GraphSelectors is Subgraph of G & the removeVertices of G,V | _GraphSelectors is removeVertices of G,V & the removeVertices of G,V | _GraphSelectors is plain )
thus ( the removeVertices of G,V | _GraphSelectors is Subgraph of G & the removeVertices of G,V | _GraphSelectors is removeVertices of G,V & the removeVertices of G,V | _GraphSelectors is plain ) by GLIB_000:128, GLIB_000:101; :: thesis: verum