let G be _Graph; :: thesis: the_Vertices_of (G .allSpanningForests()) = {(the_Vertices_of G)}
G .allSpanningForests() = (G .allSpanningSG()) /\ (G .allForests()) by Th103;
then G .allSpanningForests() c= G .allSpanningSG() by XBOOLE_1:17;
then the_Vertices_of (G .allSpanningForests()) c= the_Vertices_of (G .allSpanningSG()) by GLIBPRE1:115;
then the_Vertices_of (G .allSpanningForests()) c= {(the_Vertices_of G)} by Th75;
hence the_Vertices_of (G .allSpanningForests()) = {(the_Vertices_of G)} by ZFMISC_1:33; :: thesis: verum