let G be _Graph; :: thesis: for X being set
for E being Subset of (the_Edges_of G)
for H being reverseEdgeDirections of G,X holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
let X be set ; :: thesis: for E being Subset of (the_Edges_of G)
for H being reverseEdgeDirections of G,X holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
let E be Subset of (the_Edges_of G); :: thesis: for H being reverseEdgeDirections of G,X holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
let H be reverseEdgeDirections of G,X; :: thesis: ( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )
thus ( E is RepEdgeSelection of G implies E is RepEdgeSelection of H ) by Lm3; :: thesis: ( E is RepEdgeSelection of H implies E is RepEdgeSelection of G )
A1: G is reverseEdgeDirections of H,X by GLIB_007:3;
assume E is RepEdgeSelection of H ; :: thesis: E is RepEdgeSelection of G
hence E is RepEdgeSelection of G by A1, Lm3; :: thesis: verum