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