for G1, G2 being _Graph st G1 == G2 holds
( ( G1 is with_max_degree implies G2 is with_max_degree ) & ( G1 is with_max_in_degree implies G2 is with_max_in_degree ) & ( G1 is with_max_out_degree implies G2 is with_max_out_degree ) )