let f be PVertexMapping of G1,G2; :: thesis: ( f is continuous implies f is Dcontinuous )
assume A4: f is continuous ; :: thesis: f is Dcontinuous
consider v0 being Vertex of G1 such that
A5: the_Vertices_of G1 = {v0} by GLIB_000:22;
let v, w, e9 be object ; :: according to GLIB_011:def 4 :: 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 A6: ( 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 e9 Joins f . v,f . w,G2 by GLIB_000:16;
then consider e being object such that
A7: e Joins v,w,G1 by A4, A6, Th2;
take e ; :: thesis: e DJoins v,w,G1
( v = v0 & w = v0 ) by A5, A6, TARSKI:def 1;
hence e DJoins v,w,G1 by A7, GLIB_000:16; :: thesis: verum