theorem Th16: :: GLIB_010:16

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) holds
( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) )