for G1, G2 being _Graph holds
( ( G2 is Subgraph of G1 & G2 is Supergraph of G1 ) iff G1 == G2 )