let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( ( G1 is with_max_in_degree implies G2 is with_max_in_degree ) & ( G2 is with_max_in_degree implies G1 is with_max_in_degree ) & ( G1 is with_max_out_degree implies G2 is with_max_out_degree ) & ( G2 is with_max_out_degree implies G1 is with_max_out_degree ) )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism implies ( ( G1 is with_max_in_degree implies G2 is with_max_in_degree ) & ( G2 is with_max_in_degree implies G1 is with_max_in_degree ) & ( G1 is with_max_out_degree implies G2 is with_max_out_degree ) & ( G2 is with_max_out_degree implies G1 is with_max_out_degree ) ) )
assume A1: F is Disomorphism ; :: thesis: ( ( G1 is with_max_in_degree implies G2 is with_max_in_degree ) & ( G2 is with_max_in_degree implies G1 is with_max_in_degree ) & ( G1 is with_max_out_degree implies G2 is with_max_out_degree ) & ( G2 is with_max_out_degree implies G1 is with_max_out_degree ) )

hereby :: thesis: ( ( G2 is with_max_in_degree implies G1 is with_max_in_degree ) & ( G1 is with_max_out_degree implies G2 is with_max_out_degree ) & ( G2 is with_max_out_degree implies G1 is with_max_out_degree ) )

assume G1 is with_max_in_degree ; :: thesis: G2 is with_max_in_degree
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:92;
then ((F _V) /. v) .inDegree() = G2 .supInDegree() by A1, A2, Th60;
hence G2 is with_max_in_degree by Lm4; :: thesis: verum

end;

hereby :: thesis: ( G1 is with_max_out_degree iff G2 is with_max_out_degree )

assume G2 is with_max_in_degree ; :: thesis: G1 is with_max_in_degree
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:92;
then v0 .inDegree() = G1 .supInDegree() by A1, A3, Th60;
hence G1 is with_max_in_degree by Lm4; :: thesis: verum

end;

hereby :: thesis: ( G2 is with_max_out_degree implies G1 is with_max_out_degree )

assume G1 is with_max_out_degree ; :: thesis: G2 is with_max_out_degree
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:92;
then ((F _V) /. v) .outDegree() = G2 .supOutDegree() by A1, A5, Th60;
hence G2 is with_max_out_degree by Lm5; :: thesis: verum

end;

hereby :: thesis: verum

assume G2 is with_max_out_degree ; :: thesis: G1 is with_max_out_degree
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:92;
then v0 .outDegree() = G1 .supOutDegree() by A1, A6, Th60;
hence G1 is with_max_out_degree by Lm5; :: thesis: verum

end;