take G = the GraphUnion of S | _GraphSelectors; :: thesis: ( G is GraphUnion of S & G is plain )
thus ( G is GraphUnion of S & G is plain ) by Th22, GLIB_000:128; :: thesis: verum