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