let GSq be GraphSeq; :: thesis: ( GSq is trivial & GSq is loopless implies GSq is Tree-like )
assume A2: ( GSq is trivial & GSq is loopless ) ; :: 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 loopless trivial _Graph by A2;
G is Tree-like ;
hence GSq . n is Tree-like ; :: thesis: verum