let G be finite Graph; :: thesis: for P being oriented Chain of G holds AcyclicPaths P is finite
let P be oriented Chain of G; :: thesis: AcyclicPaths P is finite
AcyclicPaths P c= AcyclicPaths G by Th36;
hence AcyclicPaths P is finite ; :: thesis: verum