let F be PGraphMapping of G1,G2; :: thesis: ( F is directed & F is semi-continuous implies F is semi-Dcontinuous )
assume A1: ( F is directed & F is semi-continuous ) ; :: thesis: F is semi-Dcontinuous
let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 implies e DJoins v,w,G1 )
assume A2: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( not (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 or e DJoins v,w,G1 )
assume A3: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ; :: thesis: e DJoins v,w,G1
then (F _E) . e Joins (F _V) . v,(F _V) . w,G2 by GLIB_000:16;
then A4: e Joins v,w,G1 by A1, A2;
assume not e DJoins v,w,G1 ; :: thesis: contradiction
then e DJoins w,v,G1 by A4, GLIB_000:16;
then (F _E) . e DJoins (F _V) . w,(F _V) . v,G2 by A1, A2;
then (the_Source_of G2) . ((F _E) . e) = (F _V) . w by GLIB_000:def 14;
then (F _V) . v = (F _V) . w by A3, GLIB_000:def 14;
then (F _E) . e Joins (F _V) . v,(F _V) . v,G2 by A3, GLIB_000:16;
hence contradiction by GLIB_000:18; :: thesis: verum