set H0 = the spanning acyclic Subgraph of G;
set H = the spanning acyclic Subgraph of G | _GraphSelectors;
A1: the spanning acyclic Subgraph of G | _GraphSelectors == the spanning acyclic Subgraph of G by GLIB_009:9;
then the spanning acyclic Subgraph of G | _GraphSelectors is Subgraph of the spanning acyclic Subgraph of G by GLIB_000:87;
then reconsider H = the spanning acyclic Subgraph of G | _GraphSelectors as Subgraph of G by GLIB_000:43;
take H ; :: thesis: ( H is plain & H is spanning & H is acyclic )
the_Vertices_of H = the_Vertices_of the spanning acyclic Subgraph of G by A1, GLIB_000:def 34
.= the_Vertices_of G by GLIB_000:def 33 ;
hence ( H is plain & H is spanning & H is acyclic ) by A1, GLIB_002:44, GLIB_000:def 33; :: thesis: verum