let G1, G2 be _Graph; :: thesis: for x being set st G1 == G2 & x is VertexSeq of G1 holds
x is VertexSeq of G2
let x be set ; :: thesis: ( G1 == G2 & x is VertexSeq of G1 implies x is VertexSeq of G2 )
assume A1: ( G1 == G2 & x is VertexSeq of G1 ) ; :: thesis: x is VertexSeq of G2
then reconsider x2 = x as FinSequence of the_Vertices_of G2 by GLIB_000:def 36;

now

let n be Element of NAT ; :: thesis: ( 1 <= n & n < len x2 implies ex e being set st e Joins x2 . n,x2 . (n + 1),G2 )
assume ( 1 <= n & n < len x2 ) ; :: thesis: ex e being set st e Joins x2 . n,x2 . (n + 1),G2
then consider e being set such that
A2: e Joins x2 . n,x2 . (n + 1),G1 by A1, Def1;
e Joins x2 . n,x2 . (n + 1),G2 by A1, A2, GLIB_000:91;
hence ex e being set st e Joins x2 . n,x2 . (n + 1),G2 ; :: thesis: verum

end;

hence x is VertexSeq of G2 by Def1; :: thesis: verum