:: deftheorem Def37 defines inducedSubgraph GLIB_000:def 37 :
for G being _Graph
for V, E being set
for b₄ being Subgraph of G holds
( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ( b₄ is inducedSubgraph of G,V,E iff ( the_Vertices_of b₄ = V & the_Edges_of b₄ = E ) ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ( b₄ is inducedSubgraph of G,V,E iff b₄ == G ) ) );