theorem Th81: :: GLIBPRE1:80

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 v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto holds
G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1)