let f be PVertexMapping of G1,G2; f is directed
consider v0 being Vertex of G1 such that
A1:
the_Vertices_of G1 = {v0}
by GLIB_000:22;
let v, w, e be object ; GLIB_011:def 2 ( v in dom f & w in dom f & e DJoins v,w,G1 implies ex e9 being object st e9 DJoins f . v,f . w,G2 )
assume A2:
( v in dom f & w in dom f & e DJoins v,w,G1 )
; ex e9 being object st e9 DJoins f . v,f . w,G2
then
e Joins v,w,G1
by GLIB_000:16;
then consider e9 being object such that
A3:
e9 Joins f . v,f . w,G2
by A2, Th1;
take
e9
; e9 DJoins f . v,f . w,G2
( v = v0 & w = v0 )
by A1, A2, TARSKI:def 1;
hence
e9 DJoins f . v,f . w,G2
by A3, GLIB_000:16; verum