take G = the GraphMeet of G1,G2 | _GraphSelectors; :: thesis: ( G is Subgraph of G1 & G is GraphMeet of G1,G2 & G is plain )
thus ( G is Subgraph of G1 & G is GraphMeet of G1,G2 & G is plain ) by Th43, GLIB_000:128; :: thesis: verum