theorem Th20: :: GLIB_010:20

for G1, G2 being _Graph
for F being semi-Dcontinuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds
F is Dcontinuous