let G be Graph; :: thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= OrientedPaths (v1,v2)
let v1, v2 be Element of G; :: thesis: AcyclicPaths (v1,v2) c= OrientedPaths (v1,v2)
let x be object ; :: 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 and
A2: p is_acyclicpath_of v1,v2 ;
p is_orientedpath_of v1,v2 by A2;
hence x in OrientedPaths (v1,v2) by A1; :: thesis: verum