let GSq be GraphSeq; :: thesis: ( GSq is acyclic & GSq is connected implies GSq is Tree-like )
assume A5: ( GSq is acyclic & GSq is connected ) ; :: thesis: GSq is Tree-like
let n be Nat; :: according to GLIB_002:def 14 :: thesis: GSq . n is Tree-like
reconsider G = GSq . n as connected acyclic _Graph by A5, Def12, Def13;
G is Tree-like ;
hence GSq . n is Tree-like ; :: thesis: verum