let G be Graph; :: thesis: for v1, v2 being Element of the carrier of G holds AcyclicPaths v1,v2 c= AcyclicPaths G
let v1, v2 be Element of the carrier of G; :: thesis: AcyclicPaths v1,v2 c= AcyclicPaths G
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in AcyclicPaths v1,v2 or e in AcyclicPaths G )
assume e in AcyclicPaths v1,v2 ; :: thesis: e in AcyclicPaths G
then consider q being oriented Simple Chain of G such that
A1: ( e = q & q is_acyclicpath_of v1,v2 ) ;
thus e in AcyclicPaths G by A1; :: thesis: verum