let V be set ; :: thesis: for G being Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G
let G be Graph; :: thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G
let v1, v2 be Element of G; :: thesis: AcyclicPaths (v1,v2,V) c= AcyclicPaths G
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in AcyclicPaths (v1,v2,V) or e in AcyclicPaths G )
assume e in AcyclicPaths (v1,v2,V) ; :: thesis: e in AcyclicPaths G
then ex q being oriented Simple Chain of G st
( e = q & q is_acyclicpath_of v1,v2,V ) ;
hence e in AcyclicPaths G ; :: thesis: verum