let G be _Graph; :: thesis: ( G is Tree-like iff G .allSpanningTrees() = {(G | _GraphSelectors)} )

hereby :: thesis: ( G .allSpanningTrees() = {(G | _GraphSelectors)} implies G is Tree-like )

assume A1: G is Tree-like ; :: thesis: G .allSpanningTrees() = {(G | _GraphSelectors)}

now :: thesis: for x being object holds
( ( x in G .allSpanningTrees() implies x = G | _GraphSelectors ) & ( x = G | _GraphSelectors implies x in G .allSpanningTrees() ) )

let x be object ; :: thesis: ( ( x in G .allSpanningTrees() implies x = G | _GraphSelectors ) & ( x = G | _GraphSelectors implies x in G .allSpanningTrees() ) )

hereby :: thesis: ( x = G | _GraphSelectors implies x in G .allSpanningTrees() )

assume A2: x in G .allSpanningTrees() ; :: thesis: x = G | _GraphSelectors
then reconsider G9 = x as spanning plain Subgraph of G by Th168;
A3: G == G9 by A1, A2, GLIBPRE1:40;
G == G | _GraphSelectors by GLIB_000:128;
hence x = G | _GraphSelectors by A3, GLIB_000:85, GLIB_009:44; :: thesis: verum

end;

assume x = G | _GraphSelectors ; :: thesis: x in G .allSpanningTrees()
hence x in G .allSpanningTrees() by A1, Th172; :: thesis: verum

end;

hence G .allSpanningTrees() = {(G | _GraphSelectors)} by TARSKI:def 1; :: thesis: verum

end;

assume G .allSpanningTrees() = {(G | _GraphSelectors)} ; :: thesis: G is Tree-like
then G | _GraphSelectors in G .allSpanningTrees() by TARSKI:def 1;
then A4: ( G | _GraphSelectors is connected & G | _GraphSelectors is acyclic ) by Th168;
G == G | _GraphSelectors by GLIB_000:128;
hence G is Tree-like by A4, GLIB_002:48; :: thesis: verum