let G1, G2 be _Graph; :: thesis: for F being directed PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds
F is Dcontinuous
let F be directed PGraphMapping of G1,G2; :: thesis: ( F _V is one-to-one & rng (F _E) = the_Edges_of G2 implies F is Dcontinuous )
assume A1: ( F _V is one-to-one & rng (F _E) = the_Edges_of G2 ) ; :: thesis: F is Dcontinuous
then F is semi-Dcontinuous by Th18;
hence F is Dcontinuous by A1, Th20; :: thesis: verum