theorem Th8: :: GLIB_011:8

for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is continuous holds
for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))