let GSq be GraphSeq; :: thesis: ( GSq is Tree-like implies ( GSq is acyclic & GSq is connected ) )
assume A2: GSq is Tree-like ; :: thesis: ( GSq is acyclic & GSq is connected )

now :: thesis: for n being Nat holds
( GSq . n is acyclic & GSq . n is connected )

let n be Nat; :: thesis: ( GSq . n is acyclic & GSq . n is connected )
reconsider G = GSq . n as Tree-like _Graph by A2;
G is acyclic ;
hence ( GSq . n is acyclic & GSq . n is connected ) ; :: thesis: verum

end;

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