let G be non edgeless _Graph; :: thesis: 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()
let e be Edge of G; :: thesis: 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()
let V be Subset of (the_Vertices_of G); :: thesis: for H being plain addVertices of createGraph e,V st not e in G .loops() holds
H in G .allForests()
let H be plain addVertices of createGraph e,V; :: thesis: ( not e in G .loops() implies H in G .allForests() )
assume not e in G .loops() ; :: thesis: H in G .allForests()
then A1: createGraph e is acyclic by Th18;
H is Subgraph of G by Th21;
hence H in G .allForests() by A1, Th78; :: thesis: verum