:: deftheorem defines AcyclicPaths GRAPH_5:def 11 :
for G being Graph holds AcyclicPaths G = { q where q is oriented Simple Chain of G : verum } ;