for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2 st F is onto holds
card (G2 .loops()) c= card (G1 .loops())