let G be _Graph; :: thesis: ( G is Tree-like iff G | _GraphSelectors in G .allSpanningTrees() )
A1: G .allSpanningTrees() = (G .allSpanningSG()) /\ (G .allTrees()) by Th169;

hereby :: thesis: ( G | _GraphSelectors in G .allSpanningTrees() implies G is Tree-like )

assume G is Tree-like ; :: thesis: G | _GraphSelectors in G .allSpanningTrees()
then A2: G | _GraphSelectors in G .allTrees() by Th141;
G | _GraphSelectors in G .allSpanningSG() by Th62;
hence G | _GraphSelectors in G .allSpanningTrees() by A1, A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume G | _GraphSelectors in G .allSpanningTrees() ; :: thesis: G is Tree-like
then G | _GraphSelectors in G .allTrees() by A1;
hence G is Tree-like by Th141; :: thesis: verum