let V be set ; :: thesis: for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
AcyclicPaths p c= AcyclicPaths (v1,v2,V)
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,V holds
AcyclicPaths p c= AcyclicPaths (v1,v2,V)
let v1, v2 be Element of G; :: thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
AcyclicPaths p c= AcyclicPaths (v1,v2,V)
let p be oriented Chain of G; :: thesis: ( p is_orientedpath_of v1,v2,V implies AcyclicPaths p c= AcyclicPaths (v1,v2,V) )
assume A1: p is_orientedpath_of v1,v2,V ; :: thesis: AcyclicPaths p c= AcyclicPaths (v1,v2,V)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in AcyclicPaths p or x in AcyclicPaths (v1,v2,V) )
assume x in AcyclicPaths p ; :: thesis: x in AcyclicPaths (v1,v2,V)
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
A4: rng q c= rng p ;
(vertices p) \ {v2} c= V by A1;
then A5: (vertices q) \ {v2} c= V by A4, Th20;
p is_orientedpath_of v1,v2 by A1;
then ( the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) ;
then q is_orientedpath_of v1,v2 by A3;
then q is_orientedpath_of v1,v2,V by A5;
then q is_acyclicpath_of v1,v2,V ;
hence x in AcyclicPaths (v1,v2,V) by A2; :: thesis: verum