for G1, G2 being _Graph st G1 == G2 holds
for u1, v1 being Vertex of G1 st u1,v1 are_adjacent holds
for u2, v2 being Vertex of G2 st u1 = u2 & v1 = v2 holds
u2,v2 are_adjacent