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