let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds
card (G1 .loops()) = card (G2 .loops())
let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies card (G1 .loops()) = card (G2 .loops()) )
assume F is isomorphism ; :: thesis: card (G1 .loops()) = card (G2 .loops())
then ( card (G1 .loops()) c= card (G2 .loops()) & card (G2 .loops()) c= card (G1 .loops()) ) by Th92, Th93;
hence card (G1 .loops()) = card (G2 .loops()) by XBOOLE_0:def 10; :: thesis: verum