let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 st F is onto holds

card (G2 .loops()) c= card (G1 .loops())

let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is onto implies card (G2 .loops()) c= card (G1 .loops()) )

reconsider F2 = F " as one-to-one PGraphMapping of G2,G1 ;

assume F is onto ; :: thesis: card (G2 .loops()) c= card (G1 .loops())

then F2 is total by Th72;

hence card (G2 .loops()) c= card (G1 .loops()) by Th92; :: thesis: verum

card (G2 .loops()) c= card (G1 .loops())

let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is onto implies card (G2 .loops()) c= card (G1 .loops()) )

reconsider F2 = F " as one-to-one PGraphMapping of G2,G1 ;

assume F is onto ; :: thesis: card (G2 .loops()) c= card (G1 .loops())

then F2 is total by Th72;

hence card (G2 .loops()) c= card (G1 .loops()) by Th92; :: thesis: verum