thus not G .allSpanningTrees() is empty by Th173; :: thesis: ( G .allSpanningTrees() is Tree-like & G .allSpanningTrees() is simple )
G .allSpanningTrees() = (G .allSpanningSG()) /\ (G .allTrees()) by Th169;
hence ( G .allSpanningTrees() is Tree-like & G .allSpanningTrees() is simple ) ; :: thesis: verum