for G1, G2 being _Graph holds
( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) by Th41;