theorem :: GLENUM00:20

for G being non edgeless _Graph
for e being Edge of G
for H being inducedSubgraph of G,{((the_Source_of G) . e),((the_Target_of G) . e)},{e} holds H == createGraph e