theorem :: GLIB_001:177

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