let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies ( ( 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 ) ) )
assume G1 == G2 ; :: thesis: ( ( 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 ) )
then consider F being PGraphMapping of G1,G2 such that
A1: ( F = id G1 & F is Disomorphism ) by GLIBPRE0:77;
thus ( ( 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 ) ) by A1, Th83, Th84; :: thesis: verum