set G2 = the inducedSubgraph of G,V,E;

set G3 = the inducedSubgraph of G,V,E | _GraphSelectors;

take the inducedSubgraph of G,V,E | _GraphSelectors ; :: thesis: ( the inducedSubgraph of G,V,E | _GraphSelectors is Subgraph of G & the inducedSubgraph of G,V,E | _GraphSelectors is inducedSubgraph of G,V,E & the inducedSubgraph of G,V,E | _GraphSelectors is plain )

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

set G3 = the inducedSubgraph of G,V,E | _GraphSelectors;

take the inducedSubgraph of G,V,E | _GraphSelectors ; :: thesis: ( the inducedSubgraph of G,V,E | _GraphSelectors is Subgraph of G & the inducedSubgraph of G,V,E | _GraphSelectors is inducedSubgraph of G,V,E & the inducedSubgraph of G,V,E | _GraphSelectors is plain )

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