for G1, G2 being _Graph st G1 == G2 holds
( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )