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

assume A8: F is continuous ; :: thesis: F is Dcontinuous

consider u being Vertex of G1 such that

A9: the_Vertices_of G1 = {u} by GLIB_000:22;

assume A8: F is continuous ; :: thesis: F is Dcontinuous

consider u being Vertex of G1 such that

A9: the_Vertices_of G1 = {u} by GLIB_000:22;

now :: thesis: for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

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

hence
F is Dcontinuous
; :: thesis: verumex e being object st

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

let e9, v, w be object ; :: 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 A10: ( 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 A11: ( v = u & w = u ) by A9, TARSKI:def 1;

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

then consider e being object such that

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

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

( e DJoins v,w,G1 or e DJoins w,v,G1 ) by A12, GLIB_000:16;

hence ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A11, A12; :: thesis: verum

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

assume A10: ( 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 A11: ( v = u & w = u ) by A9, TARSKI:def 1;

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

then consider e being object such that

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

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

( e DJoins v,w,G1 or e DJoins w,v,G1 ) by A12, GLIB_000:16;

hence ( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) by A11, A12; :: thesis: verum