let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() )
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() ) )
assume A1: F is isomorphism ; :: thesis: ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() )
then rng (F _V) = the_Vertices_of G2 by GLIB_010:def 12;
then A2: ( G1 .supDegree() c= G2 .supDegree() & G1 .minDegree() c= G2 .minDegree() ) by A1, Th51, Th52;
reconsider F0 = F as one-to-one PGraphMapping of G1,G2 by A1;
A3: F0 " is isomorphism by A1, GLIB_010:75;
then rng ((F0 ") _V) = the_Vertices_of G1 by GLIB_010:def 12;
then ( G2 .supDegree() c= G1 .supDegree() & G2 .minDegree() c= G1 .minDegree() ) by A3, Th51, Th52;
hence ( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() ) by A2, XBOOLE_0:def 10; :: thesis: verum