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