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