theorem Th82: :: GLIBPRE1:81

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2