thus not G .allSpanningForests() is empty by Th106; :: thesis: ( G .allSpanningForests() is \/-tolerating & G .allSpanningForests() is plain & G .allSpanningForests() is acyclic & G .allSpanningForests() is simple )
G .allSpanningForests() = (G .allSpanningSG()) /\ (G .allForests()) by Th103;
hence ( G .allSpanningForests() is \/-tolerating & G .allSpanningForests() is plain & G .allSpanningForests() is acyclic & G .allSpanningForests() is simple ) ; :: thesis: verum