let G be finite Graph; :: thesis: AcyclicPaths G is finite
set n = EdgesCount G;
set D = the carrier' of G;
set A = { x where x is Element of the carrier' of G * : len x <= EdgesCount G } ;
A1: AcyclicPaths G c= { x where x is Element of the carrier' of G * : len x <= EdgesCount G }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in AcyclicPaths G or x in { x where x is Element of the carrier' of G * : len x <= EdgesCount G } )
assume x in AcyclicPaths G ; :: thesis: x in { x where x is Element of the carrier' of G * : len x <= EdgesCount G }
then consider p being oriented Simple Chain of G such that
A2: x = p ;
( p is Element of the carrier' of G * & len p <= EdgesCount G ) by Th56, FINSEQ_1:def 11;
hence x in { x where x is Element of the carrier' of G * : len x <= EdgesCount G } by A2; :: thesis: verum

end;

{ x where x is Element of the carrier' of G * : len x <= EdgesCount G } is finite by Th3;
hence AcyclicPaths G is finite by A1; :: thesis: verum