let F be PGraphMapping of G1,G2; ( F is directed & F is continuous implies F is Dcontinuous )
assume A5:
( F is directed & F is continuous )
; F is Dcontinuous
let e9, v, w be object ; GLIB_010:def 18 ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 implies ex e being object st
( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) )
assume A6:
( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 )
; ex e being object st
( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
then A7:
e9 Joins (F _V) . v,(F _V) . w,G2
by GLIB_000:16;
then consider e being object such that
A8:
( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
by A5, A6;
take
e
; ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
not e DJoins w,v,G1
hence
( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
by A8, GLIB_000:16; verum