theorem :: GLIBPRE0:73

for G being _Graph
for V being set
for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )