theorem :: GLIB_010:37

for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st F is onto & G1 is loopless holds
G2 is loopless by Th36;