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