let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st ( for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & v,w are_adjacent holds
ex e being object st
( e in dom (F _E) & e Joins v,w,G1 ) ) holds
F _V is PVertexMapping of G1,G2
let F be PGraphMapping of G1,G2; :: thesis: ( ( for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & v,w are_adjacent holds
ex e being object st
( e in dom (F _E) & e Joins v,w,G1 ) ) implies F _V is PVertexMapping of G1,G2 )
assume A1: for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & v,w are_adjacent holds
ex e being object st
( e in dom (F _E) & e Joins v,w,G1 ) ; :: thesis: F _V is PVertexMapping of G1,G2
let v, w be Vertex of G1; :: according to GLIB_011:def 1 :: thesis: ( v in dom (F _V) & w in dom (F _V) & v,w are_adjacent implies (F _V) /. v,(F _V) /. w are_adjacent )
assume A2: ( v in dom (F _V) & w in dom (F _V) & v,w are_adjacent ) ; :: thesis: (F _V) /. v,(F _V) /. w are_adjacent
then consider e being object such that
A3: ( e in dom (F _E) & e Joins v,w,G1 ) by A1;
A4: ( (F _V) /. v = (F _V) . v & (F _V) /. w = (F _V) . w ) by A2, PARTFUN1:def 6;
(F _E) . e Joins (F _V) . v,(F _V) . w,G2 by A2, A3, GLIB_010:4;
hence (F _V) /. v,(F _V) /. w are_adjacent by A4, CHORD:def 3; :: thesis: verum