let f be PVertexMapping of G1,G2; :: thesis: ( f is Dcontinuous implies f is continuous )
assume A1: f is Dcontinuous ; :: thesis: f is continuous

now :: thesis: for v, w, e9 being object st v in dom f & w in dom f & e9 Joins f . v,f . w,G2 holds
ex e being object st e Joins v,w,G1

let v, w, e9 be object ; :: thesis: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 implies ex e being object st b₄ Joins e,b₂,G1 )
assume A2: ( v in dom f & w in dom f & e9 Joins f . v,f . w,G2 ) ; :: thesis: ex e being object st b₄ Joins e,b₂,G1

per cases then ( e9 DJoins f . v,f . w,G2 or e9 DJoins f . w,f . v,G2 ) by GLIB_000:16;

suppose e9 DJoins f . v,f . w,G2 ; :: thesis: ex e being object st b₄ Joins e,b₂,G1

then consider e being object such that
A3: e DJoins v,w,G1 by A1, A2;
take e = e; :: thesis: e Joins v,w,G1
thus e Joins v,w,G1 by A3, GLIB_000:16; :: thesis: verum

end;

suppose e9 DJoins f . w,f . v,G2 ; :: thesis: ex e being object st b₄ Joins e,b₂,G1

then consider e being object such that
A4: e DJoins w,v,G1 by A1, A2;
take e = e; :: thesis: e Joins v,w,G1
thus e Joins v,w,G1 by A4, GLIB_000:16; :: thesis: verum

end;

end;

end;

hence f is continuous by Th2; :: thesis: verum