let G be _Graph; :: thesis: createGraph ([#] (the_Vertices_of G)) in G .allSpanningForests()
set H = createGraph ([#] (the_Vertices_of G));
A1: createGraph ([#] (the_Vertices_of G)) in G .allForests() by Th81;
A2: createGraph ([#] (the_Vertices_of G)) in G .allSpanningSG() by Th63;
G .allSpanningForests() = (G .allSpanningSG()) /\ (G .allForests()) by Th103;
hence createGraph ([#] (the_Vertices_of G)) in G .allSpanningForests() by A1, A2, XBOOLE_0:def 4; :: thesis: verum