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