let v, w be Vertex of G1; :: thesis: ( v <> w implies v,w are_adjacent )
assume A3: v <> w ; :: thesis: v,w are_adjacent
( v in the_Vertices_of G1 & w in the_Vertices_of G1 ) ;
then A4: ( v in dom (F _V) & w in dom (F _V) ) by A1, Def11;
then ( (F _V) . v in rng (F _V) & (F _V) . w in rng (F _V) ) by FUNCT_1:3;
then reconsider v2 = (F _V) . v, w2 = (F _V) . w as Vertex of G2 ;
v2 <> w2 by A1, A3, A4, FUNCT_1:def 4;
then consider e2 being object such that
A5: e2 Joins v2,w2,G2 by A2, CHORD:def 6, CHORD:def 3;
consider e1 being object such that
A6: ( e1 Joins v,w,G1 & e1 in dom (F _E) & (F _E) . e1 = e2 ) by A1, A4, A5, Def16;
thus v,w are_adjacent by A6, CHORD:def 3; :: thesis: verum