theorem Th80: :: GLIB_009:80

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