let G1, G2 be _Graph; for x being set st G1 == G2 & x is EdgeSeq of G1 holds
x is EdgeSeq of G2
let x be set ; ( G1 == G2 & x is EdgeSeq of G1 implies x is EdgeSeq of G2 )
assume that
A1:
G1 == G2
and
A2:
x is EdgeSeq of G1
; x is EdgeSeq of G2
reconsider es = x as EdgeSeq of G1 by A2;
reconsider es2 = es as FinSequence of the_Edges_of G2 by A1, GLIB_000:def 34;
consider vs being FinSequence of the_Vertices_of G1 such that
A3:
len vs = (len es) + 1
and
A4:
for n being Element of NAT st 1 <= n & n <= len es holds
es . n Joins vs . n,vs . (n + 1),G1
by Def2;
now ex vs being FinSequence of the_Vertices_of G2 st
( len vs = (len es) + 1 & ( for n being Element of NAT st 1 <= n & n <= len es2 holds
es2 . n Joins vs . n,vs . (n + 1),G2 ) )reconsider vs =
vs as
FinSequence of
the_Vertices_of G2 by A1, GLIB_000:def 34;
take vs =
vs;
( len vs = (len es) + 1 & ( for n being Element of NAT st 1 <= n & n <= len es2 holds
es2 . n Joins vs . n,vs . (n + 1),G2 ) )thus
len vs = (len es) + 1
by A3;
for n being Element of NAT st 1 <= n & n <= len es2 holds
es2 . n Joins vs . n,vs . (n + 1),G2let n be
Element of
NAT ;
( 1 <= n & n <= len es2 implies es2 . n Joins vs . n,vs . (n + 1),G2 )assume that A5:
1
<= n
and A6:
n <= len es2
;
es2 . n Joins vs . n,vs . (n + 1),G2
es2 . n Joins vs . n,
vs . (n + 1),
G1
by A4, A5, A6;
hence
es2 . n Joins vs . n,
vs . (n + 1),
G2
by A1, GLIB_000:88;
verum end;
hence
x is EdgeSeq of G2
by Def2; verum