let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds

( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( G1 .order() = G2 .order() & G1 .size() = G2 .size() ) )

assume A1: F is isomorphism ; :: thesis: ( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

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

A2: ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) by A1, Th45;

F " is isomorphism by A1, Th75;

then ( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() ) by Th45;

hence ( G1 .order() = G2 .order() & G1 .size() = G2 .size() ) by A2, XBOOLE_0:def 10; :: thesis: verum

( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( G1 .order() = G2 .order() & G1 .size() = G2 .size() ) )

assume A1: F is isomorphism ; :: thesis: ( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

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

A2: ( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() ) by A1, Th45;

F " is isomorphism by A1, Th75;

then ( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() ) by Th45;

hence ( G1 .order() = G2 .order() & G1 .size() = G2 .size() ) by A2, XBOOLE_0:def 10; :: thesis: verum