:: deftheorem Def4 defines createGraph GLENUM00:def 4 :
for G being non edgeless _Graph
for e being Edge of G
for b₃ being plain Subgraph of G holds
( b₃ = createGraph e iff ex V being non empty Subset of (the_Vertices_of G) ex S, T being Function of {e},V st
( b₃ = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) ) );