let G be Graph; :: thesis: for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
AcyclicPaths p c= AcyclicPaths v1,v2
let v1, v2 be Element of G; :: thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
AcyclicPaths p c= AcyclicPaths v1,v2
let p be oriented Chain of G; :: thesis: ( p is_orientedpath_of v1,v2 implies AcyclicPaths p c= AcyclicPaths v1,v2 )
assume p is_orientedpath_of v1,v2 ; :: thesis: AcyclicPaths p c= AcyclicPaths v1,v2
then A1: ( the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by Def3;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in AcyclicPaths p or x in AcyclicPaths v1,v2 )
assume x in AcyclicPaths p ; :: thesis: x in AcyclicPaths v1,v2
then consider q being oriented Simple Chain of G such that
A2: x = q and
A3: ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) ) and
rng q c= rng p ;
q is_orientedpath_of v1,v2 by A1, A3, Def3;
then q is_acyclicpath_of v1,v2 by Def6;
hence x in AcyclicPaths v1,v2 by A2; :: thesis: verum