let V be set ; :: thesis: for G being finite Graph
for v1, v2 being Element of G holds AcyclicPaths v1,v2,V is finite
let G be finite Graph; :: thesis: for v1, v2 being Element of G holds AcyclicPaths v1,v2,V is finite
let v1, v2 be Element of G; :: thesis: AcyclicPaths v1,v2,V is finite
AcyclicPaths v1,v2,V c= AcyclicPaths G by Th49;
hence AcyclicPaths v1,v2,V is finite ; :: thesis: verum