let F be PGraphMapping of G1,G2; 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 ;
( 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) )
;
( 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
;
(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;
verum
end;
hence
F is directed
; verum