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 ) ;
let x be object ; :: 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;
then q is_acyclicpath_of v1,v2 ;
hence x in AcyclicPaths (v1,v2) by A2; :: thesis: verum