let f be PVertexMapping of G1,G2; :: thesis: ( f is Dcontinuous implies f is directed )
assume A1: f is Dcontinuous ; :: thesis: f is directed
let v, w, e be object ; :: according to GLIB_011:def 2 :: thesis: ( v in dom f & w in dom f & e DJoins v,w,G1 implies ex e9 being object st e9 DJoins f . v,f . w,G2 )
assume A2: ( v in dom f & w in dom f & e DJoins v,w,G1 ) ; :: thesis: ex e9 being object st e9 DJoins f . v,f . w,G2
then A3: e Joins v,w,G1 by GLIB_000:16;
then consider e9 being object such that
A4: e9 Joins f . v,f . w,G2 by A2, Th1;
take e9 ; :: thesis: e9 DJoins f . v,f . w,G2
assume not e9 DJoins f . v,f . w,G2 ; :: thesis: contradiction
then e9 DJoins f . w,f . v,G2 by A4, GLIB_000:16;
then consider e0 being object such that
A5: e0 DJoins w,v,G1 by A1, A2;
e0 Joins v,w,G1 by A5, GLIB_000:16;
then e = e0 by A3, GLIB_000:def 20;
then (the_Source_of G1) . e = w by A5, GLIB_000:def 14;
then v = w by A2, GLIB_000:def 14;
hence contradiction by A3, GLIB_000:18; :: thesis: verum