theorem Th8: :: GLIB_012:8

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is semi-continuous & dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) & G2 is loopfull holds
G1 is loopfull