let S be Graph-membered set ; :: thesis: ( S is acyclic & S is connected implies S is Tree-like )
assume A7: ( S is acyclic & S is connected ) ; :: thesis: S is Tree-like
let G be _Graph; :: according to GLIB_014:def 10 :: thesis: ( G in S implies G is Tree-like )
assume G in S ; :: thesis: G is Tree-like
then ( G is acyclic & G is connected ) by A7;
hence G is Tree-like ; :: thesis: verum