set G2 = the reverseEdgeDirections of G,E;
set G3 = the reverseEdgeDirections of G,E | _GraphSelectors;
take
the reverseEdgeDirections of G,E | _GraphSelectors
; ( 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 Th9, GLIB_007:2; verum