for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 holds
( (F ") _V = (F _V) " & (F ") _E = (F _E) " ) ;