take G = the GraphUnion of G1,G2 | _GraphSelectors; :: thesis: ( G is Supergraph of G1 & G is GraphUnion of G1,G2 & G is plain )
thus ( G is Supergraph of G1 & G is GraphUnion of G1,G2 & G is plain ) by Th28, GLIB_009:9; :: thesis: verum