:: deftheorem Def18 defines Dcontinuous GLIB_010:def 18 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is Dcontinuous iff 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 ) );