for G1, G2 being _Graph
for x being set st G1 == G2 & x is EdgeSeq of G1 holds
x is EdgeSeq of G2