for G1, G2 being _Graph st G1 == G2 holds
( ( G1 is vertex-finite implies G2 is vertex-finite ) & ( G1 is edge-finite implies G2 is edge-finite ) ) by GLIB_000:def 34;