:: deftheorem Def32 defines Subgraph GLIB_000:def 32 :
for G, b₂ being _Graph holds
( b₂ is Subgraph of G iff ( the_Vertices_of b₂ c= the_Vertices_of G & the_Edges_of b₂ c= the_Edges_of G & ( for e being set st e in the_Edges_of b₂ holds
( (the_Source_of b₂) . e = (the_Source_of G) . e & (the_Target_of b₂) . e = (the_Target_of G) . e ) ) ) );