let G be non edgeless _Graph; :: thesis: for e being Edge of G
for H being plain addVertices of createGraph e, the_Vertices_of G st not e in G .loops() holds
H in G .allSpanningForests()
let e be Edge of G; :: thesis: for H being plain addVertices of createGraph e, the_Vertices_of G st not e in G .loops() holds
H in G .allSpanningForests()
let H be plain addVertices of createGraph e, the_Vertices_of G; :: thesis: ( not e in G .loops() implies H in G .allSpanningForests() )
assume A1: not e in G .loops() ; :: thesis: H in G .allSpanningForests()
the_Vertices_of G c= the_Vertices_of G ;
then ( H in G .allForests() & H in G .allSpanningSG() ) by A1, Th64, Th84;
then H in (G .allForests()) /\ (G .allSpanningSG()) by XBOOLE_0:def 4;
hence H in G .allSpanningForests() by Th103; :: thesis: verum