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