let G be _Graph; :: thesis: for W being Walk of G

for m, n being Nat st W .cut (m,n) is V5() holds

not W is V5()

let W be Walk of G; :: thesis: for m, n being Nat st W .cut (m,n) is V5() holds

not W is V5()

let m, n be Nat; :: thesis: ( W .cut (m,n) is V5() implies not W is V5() )

assume that

A1: W .cut (m,n) is V5() and

A2: W is V5() ; :: thesis: contradiction

reconsider W = W as V5() Walk of G by A2;

reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;

W .cut (m9,n9) is V5() ;

hence contradiction by A1; :: thesis: verum

for m, n being Nat st W .cut (m,n) is V5() holds

not W is V5()

let W be Walk of G; :: thesis: for m, n being Nat st W .cut (m,n) is V5() holds

not W is V5()

let m, n be Nat; :: thesis: ( W .cut (m,n) is V5() implies not W is V5() )

assume that

A1: W .cut (m,n) is V5() and

A2: W is V5() ; :: thesis: contradiction

reconsider W = W as V5() Walk of G by A2;

reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;

W .cut (m9,n9) is V5() ;

hence contradiction by A1; :: thesis: verum