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