:: deftheorem Def9 defines Supergraph GLIB_006:def 9 :
for G, b₂ being _Graph holds
( b₂ is Supergraph of G iff ( the_Vertices_of G c= the_Vertices_of b₂ & the_Edges_of G c= the_Edges_of b₂ & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of b₂) . e & (the_Target_of G) . e = (the_Target_of b₂) . e ) ) ) );