let GS be GraphSeq; :: thesis: ( GS is trivial & GS is loopless implies GS is finite )
assume ( GS is trivial & GS is loopless ) ; :: thesis: GS is finite
then reconsider GS9 = GS as loopless trivial GraphSeq ;
for x being Nat holds GS9 . x is finite ;
hence GS is finite by Def60; :: thesis: verum