let F be PGraphMapping of G1,G2; :: thesis: ( F is directed & F is continuous implies F is Dcontinuous )

assume A5: ( F is directed & F is continuous ) ; :: thesis: F is Dcontinuous

let e9, v, w be object ; :: according to GLIB_010:def 18 :: thesis: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 implies ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) )

assume A6: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

then A7: e9 Joins (F _V) . v,(F _V) . w,G2 by GLIB_000:16;

then consider e being object such that

A8: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A5, A6;

take e ; :: thesis: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

not e DJoins w,v,G1

assume A5: ( F is directed & F is continuous ) ; :: thesis: F is Dcontinuous

let e9, v, w be object ; :: according to GLIB_010:def 18 :: thesis: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 implies ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) )

assume A6: ( v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 ) ; :: thesis: ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

then A7: e9 Joins (F _V) . v,(F _V) . w,G2 by GLIB_000:16;

then consider e being object such that

A8: ( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A5, A6;

take e ; :: thesis: ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )

not e DJoins w,v,G1

proof

hence
( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 )
by A8, GLIB_000:16; :: thesis: verum
assume
e DJoins w,v,G1
; :: thesis: contradiction

then e9 DJoins (F _V) . w,(F _V) . v,G2 by A5, A6, A8;

then (F _V) . v = (F _V) . w by A6, GLIB_009:6;

hence contradiction by A7, GLIB_000:18; :: thesis: verum

end;then e9 DJoins (F _V) . w,(F _V) . v,G2 by A5, A6, A8;

then (F _V) . v = (F _V) . w by A6, GLIB_009:6;

hence contradiction by A7, GLIB_000:18; :: thesis: verum