let G1, G2 be _Graph; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( u1 = u2 & v1 = v2 implies u2,v2 are_adjacent )

assume that

A3: u1 = u2 and

A4: v1 = v2 ; :: thesis: u2,v2 are_adjacent

e Joins u2,v2,G2 by A1, A3, A4, A2;

hence u2,v2 are_adjacent ; :: thesis: verum

for u2, v2 being Vertex of G2 st u1 = u2 & v1 = v2 holds

u2,v2 are_adjacent )

assume A1: G1 == G2 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( u1 = u2 & v1 = v2 implies u2,v2 are_adjacent )

assume that

A3: u1 = u2 and

A4: v1 = v2 ; :: thesis: u2,v2 are_adjacent

e Joins u2,v2,G2 by A1, A3, A4, A2;

hence u2,v2 are_adjacent ; :: thesis: verum