for G1, G2 being _Graph st G1 == G2 holds
( ( G1 is _finite implies G2 is _finite ) & ( G1 is loopless implies G2 is loopless ) & ( G1 is _trivial implies G2 is _trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) )