let G be _Graph; :: thesis: ( G is Tree-like iff G | _GraphSelectors in G .allTrees() )

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

assume A1: G is Tree-like ; :: thesis: G | _GraphSelectors in G .allTrees()
G is Subgraph of G by GLIB_000:40;
hence G | _GraphSelectors in G .allTrees() by A1, Th140; :: thesis: verum

end;

assume G | _GraphSelectors in G .allTrees() ; :: thesis: G is Tree-like
then A2: G | _GraphSelectors is Tree-like by Th138;
G | _GraphSelectors == G by GLIB_000:128;
hence G is Tree-like by A2, GLIB_002:48; :: thesis: verum