let F be PGraphMapping of G1,G2; :: thesis: F is directed
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 ;
hence F is directed by GLIB_010:def 14; :: thesis: verum