for G1, G2 being _Graph
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 ) )