theorem Th13: :: GLENUM00:13

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