let F be PGraphMapping of G1,G2; :: thesis: F is directed
consider u being Vertex of G1 such that
A1: the_Vertices_of G1 = {u} by GLIB_000:22;
for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2

proof

let e, v, w be object ; :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )
assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not e DJoins v,w,G1 or (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )
then A3: ( v = u & w = u ) by A1, TARSKI:def 1;
assume e DJoins v,w,G1 ; :: thesis: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2
then e Joins u,u,G1 by A3, GLIB_000:16;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A2, A3, Th4, GLIB_000:16; :: thesis: verum

end;

hence F is directed ; :: thesis: verum