set G2 = the removeVertex of G,v;

set G3 = the removeVertex of G,v | _GraphSelectors;

take the removeVertex of G,v | _GraphSelectors ; :: thesis: ( the removeVertex of G,v | _GraphSelectors is Subgraph of G & the removeVertex of G,v | _GraphSelectors is removeVertex of G,v & the removeVertex of G,v | _GraphSelectors is plain )

thus ( the removeVertex of G,v | _GraphSelectors is Subgraph of G & the removeVertex of G,v | _GraphSelectors is removeVertex of G,v & the removeVertex of G,v | _GraphSelectors is plain ) by Th9, GLIB_006:16; :: thesis: verum

set G3 = the removeVertex of G,v | _GraphSelectors;

take the removeVertex of G,v | _GraphSelectors ; :: thesis: ( the removeVertex of G,v | _GraphSelectors is Subgraph of G & the removeVertex of G,v | _GraphSelectors is removeVertex of G,v & the removeVertex of G,v | _GraphSelectors is plain )

thus ( the removeVertex of G,v | _GraphSelectors is Subgraph of G & the removeVertex of G,v | _GraphSelectors is removeVertex of G,v & the removeVertex of G,v | _GraphSelectors is plain ) by Th9, GLIB_006:16; :: thesis: verum