let S be Graph-membered set ; :: thesis: ( S is Tree-like implies ( S is acyclic & S is connected ) )
assume A8: S is Tree-like ; :: thesis: ( S is acyclic & S is connected )

now :: thesis: for G being _Graph st G in S holds
( G is acyclic & G is connected )

let G be _Graph; :: thesis: ( G in S implies ( G is acyclic & G is connected ) )
assume G in S ; :: thesis: ( G is acyclic & G is connected )
then G is Tree-like by A8;
hence ( G is acyclic & G is connected ) ; :: thesis: verum

end;

hence ( S is acyclic & S is connected ) ; :: thesis: verum