let G be finite Graph; :: thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2) is finite
let v1, v2 be Element of G; :: thesis: AcyclicPaths (v1,v2) is finite
AcyclicPaths (v1,v2) c= AcyclicPaths G by Th37;
hence AcyclicPaths (v1,v2) is finite ; :: thesis: verum