let G be Graph; :: thesis: for v1, v2 being Element of G
for p being oriented Chain of G st p = {} holds
not p is_acyclicpath_of v1,v2
let v1, v2 be Element of G; :: thesis: for p being oriented Chain of G st p = {} holds
not p is_acyclicpath_of v1,v2
let p be oriented Chain of G; :: thesis: ( p = {} implies not p is_acyclicpath_of v1,v2 )
assume p = {} ; :: thesis: not p is_acyclicpath_of v1,v2
then not p is_orientedpath_of v1,v2 ;
hence not p is_acyclicpath_of v1,v2 ; :: thesis: verum