let G1 be _Graph; :: thesis: ( G1 is G -isomorphic implies G1 is loopless )
assume G1 is G -isomorphic ; :: thesis: G1 is loopless
then consider F being PGraphMapping of G,G1 such that
A1: F is isomorphism by GLIB_010:def 23;
thus G1 is loopless by A1, GLIB_010:37; :: thesis: verum