let G1, G2 be _Graph; ( G1 == G2 implies 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 )
assume A1:
G1 == G2
; 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
let u1, v1 be Vertex of G1; ( u1,v1 are_adjacent implies for u2, v2 being Vertex of G2 st u1 = u2 & v1 = v2 holds
u2,v2 are_adjacent )
assume
u1,v1 are_adjacent
; for u2, v2 being Vertex of G2 st u1 = u2 & v1 = v2 holds
u2,v2 are_adjacent
then consider e being object such that
A2:
e Joins u1,v1,G1
;
let u2, v2 be Vertex of G2; ( u1 = u2 & v1 = v2 implies u2,v2 are_adjacent )
assume that
A3:
u1 = u2
and
A4:
v1 = v2
; u2,v2 are_adjacent
e Joins u2,v2,G2
by A1, A3, A4, A2;
hence
u2,v2 are_adjacent
; verum