set H0 = the Tree-like Subgraph of G;
set H = the Tree-like Subgraph of G | _GraphSelectors;
A2: the Tree-like Subgraph of G | _GraphSelectors == the Tree-like Subgraph of G by GLIB_009:9;
then the Tree-like Subgraph of G | _GraphSelectors is Subgraph of the Tree-like Subgraph of G by GLIB_000:87;
then reconsider H = the Tree-like Subgraph of G | _GraphSelectors as Subgraph of G by GLIB_000:43;
take H ; :: thesis: ( H is plain & H is Tree-like )
A3: H is acyclic by A2, GLIB_002:44;
H is connected by A2, GLIB_002:8;
hence ( H is plain & H is Tree-like ) by A3; :: thesis: verum