theorem :: GLIB_012:10

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is loopfull iff G2 is loopfull ) by Th7, Th9;