theorem Th81: :: GLIB_009:81

for G1 being _Graph
for G2 being Subgraph of G1
for E2 being RepDEdgeSelection of G2 ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)