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

now

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

end;

hence ( GSq is acyclic & GSq is connected ) by Def12, Def13; :: thesis: verum