let G1, G2 be _Graph; ( ( G2 is Subgraph of G1 & G2 is Supergraph of G1 ) iff G1 == G2 )
( G1 == G2 iff ( G2 is Subgraph of G1 & G1 is Subgraph of G2 ) )
by GLIB_000:87;
hence
( ( G2 is Subgraph of G1 & G2 is Supergraph of G1 ) iff G1 == G2 )
by Th61; verum