let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
assume A1: F is Disomorphism ; :: thesis:

hereby :: thesis:

assume G1 is with_max_in_degree ; :: thesis:
then consider v being Vertex of G1 such that
A2: v .inDegree() = G1 .supInDegree() and
for w being Vertex of G1 holds w .inDegree() c= v .inDegree() by Th80;
v .inDegree() = ((F _V) /. v) .inDegree() by A1, GLIBPRE0:94;
then ((F _V) /. v) .inDegree() = G2 .supInDegree() by A1, A2, Th60;
hence G2 is with_max_in_degree by Lm4; :: thesis:

end;

hereby :: thesis:

assume G2 is with_max_in_degree ; :: thesis:
then consider v being Vertex of G2 such that
A3: v .inDegree() = G2 .supInDegree() and
for w being Vertex of G2 holds w .inDegree() c= v .inDegree() by Th80;
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 .inDegree() = v0 .inDegree() by A1, GLIBPRE0:94;
then v0 .inDegree() = G1 .supInDegree() by A1, A3, Th60;
hence G1 is with_max_in_degree by Lm4; :: thesis:

end;

hereby :: thesis:

assume G1 is with_max_out_degree ; :: thesis:
then consider v being Vertex of G1 such that
A5: v .outDegree() = G1 .supOutDegree() and
for w being Vertex of G1 holds w .outDegree() c= v .outDegree() by Th81;
v .outDegree() = ((F _V) /. v) .outDegree() by A1, GLIBPRE0:94;
then ((F _V) /. v) .outDegree() = G2 .supOutDegree() by A1, A5, Th60;
hence G2 is with_max_out_degree by Lm5; :: thesis:

end;

hereby :: thesis:

assume G2 is with_max_out_degree ; :: thesis:
then consider v being Vertex of G2 such that
A6: v .outDegree() = G2 .supOutDegree() and
for w being Vertex of G2 holds w .outDegree() c= v .outDegree() by Th81;
rng (F _V) = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A7: ( v0 in dom (F _V) & (F _V) . v0 = v ) by FUNCT_1:def 3;
reconsider v0 = v0 as Vertex of G1 by A7;
(F _V) /. v0 = v by A7, PARTFUN1:def 6;
then v .outDegree() = v0 .outDegree() by A1, GLIBPRE0:94;
then v0 .outDegree() = G1 .supOutDegree() by A1, A6, Th60;
hence G1 is with_max_out_degree by Lm5; :: thesis:

end;