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

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

hence
F is directed
; :: thesis: verum
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;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