let G be _Graph; :: thesis: for H being spanning acyclic Subgraph of G st H is connected holds
H | _GraphSelectors in G .allSpanningTrees()
let H be spanning acyclic Subgraph of G; :: thesis: ( H is connected implies H | _GraphSelectors in G .allSpanningTrees() )
assume A1: H is connected ; :: thesis: H | _GraphSelectors in G .allSpanningTrees()
A2: H | _GraphSelectors == H by GLIB_000:128;
then H | _GraphSelectors is spanning acyclic Subgraph of G by GLIB_000:171, GLIB_002:44;
hence H | _GraphSelectors in G .allSpanningTrees() by A1, A2, Th168, GLIB_002:8; :: thesis: verum