let f be PVertexMapping of G1,G2; :: thesis: 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 ; :: according to GLIB_011:def 2 :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum