let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is with_max_degree iff G2 is with_max_degree )
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( G1 is with_max_degree iff G2 is with_max_degree ) )
assume A1: F is isomorphism ; :: thesis: ( G1 is with_max_degree iff G2 is with_max_degree )
hereby :: thesis: ( G2 is with_max_degree implies G1 is with_max_degree )
assume G1 is with_max_degree ; :: thesis: G2 is with_max_degree
then consider v being Vertex of G1 such that
A2: v .degree() = G1 .supDegree() and
for w being Vertex of G1 holds w .degree() c= v .degree() by Th79;
v .degree() = ((F _V) /. v) .degree() by A1, GLIBPRE0:95;
then ((F _V) /. v) .degree() = G2 .supDegree() by A1, A2, Th55;
hence G2 is with_max_degree by Lm3; :: thesis: verum
end;
assume G2 is with_max_degree ; :: thesis: G1 is with_max_degree
then consider v being Vertex of G2 such that
A3: v .degree() = G2 .supDegree() and
for w being Vertex of G2 holds w .degree() c= v .degree() by Th79;
rng (F _V) = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A4: ( v0 in dom (F _V) & (F _V) . v0 = v ) by FUNCT_1:def 3;
reconsider v0 = v0 as Vertex of G1 by A4;
(F _V) /. v0 = v by A4, PARTFUN1:def 6;
then v .degree() = v0 .degree() by A1, GLIBPRE0:95;
then v0 .degree() = G1 .supDegree() by A1, A3, Th55;
hence G1 is with_max_degree by Lm3; :: thesis: verum