let f be PVertexMapping of G1,G2; :: thesis: ( f is Dcontinuous & f is continuous )
consider v0 being Vertex of G2 such that
A1: the_Vertices_of G2 = {v0} by GLIB_000:22;
now :: thesis: for v, w, e9 being object st v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 holds
ex e being object st e DJoins v,w,G1
let v, w, e9 be object ; :: thesis: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 implies ex e being object st e DJoins v,w,G1 )
assume A2: ( v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 ) ; :: thesis: ex e being object st e DJoins v,w,G1
then ( f . v in rng f & f . w in rng f ) by FUNCT_1:3;
then ( f . v = v0 & f . w = v0 ) by A1, TARSKI:def 1;
then e9 Joins v0,v0,G2 by A2, GLIB_000:16;
hence ex e being object st e DJoins v,w,G1 by GLIB_000:18; :: thesis: verum
end;
hence f is Dcontinuous ; :: thesis: f is continuous
hence f is continuous ; :: thesis: verum