set G2 = the removeEdge of G,e;

set G3 = the removeEdge of G,e | _GraphSelectors;

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

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

set G3 = the removeEdge of G,e | _GraphSelectors;

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

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