let G1, G2 be _Graph; :: thesis: ( G1 is Supergraph of G2 iff G2 c= G1 )
( G1 is Supergraph of G2 iff G2 is Subgraph of G1 ) by Th61;
hence ( G1 is Supergraph of G2 iff G2 c= G1 ) by GLIB_000:def 35; :: thesis: verum