theorem Th101: :: GLIBPRE1:100

for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for V2 being non empty Subset of (the_Vertices_of (rng F))
for H being inducedSubgraph of (rng F),V2 st G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) holds
(F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H))