theorem Th84: :: GLENUM00:84

for G being non edgeless _Graph
for e being Edge of G
for V being Subset of (the_Vertices_of G)
for H being plain addVertices of createGraph e,V st not e in G .loops() holds
H in G .allForests()