let f be PVertexMapping of G1,G2; :: thesis: ( f is directed & f is continuous implies f is Dcontinuous )
assume A1: ( f is directed & f is continuous ) ; :: thesis: f is Dcontinuous
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 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 A3: e9 Joins f . v,f . w,G2 by GLIB_000:16;
then consider e being object such that
A4: e Joins v,w,G1 by A1, A2, Th2;
take e ; :: thesis: e DJoins v,w,G1
assume not e DJoins v,w,G1 ; :: thesis: contradiction
then e DJoins w,v,G1 by A4, GLIB_000:16;
then consider e0 being object such that
A5: e0 DJoins f . w,f . v,G2 by A1, A2;
e0 Joins f . v,f . w,G2 by A5, GLIB_000:16;
then e0 = e9 by A3, GLIB_000:def 20;
then (the_Source_of G2) . e9 = f . w by A5, GLIB_000:def 14;
then f . w = f . v by A2, GLIB_000:def 14;
hence contradiction by A3, GLIB_000:18; :: thesis: verum