let G be _Graph; :: thesis: for W being Walk of G
for m, n being Nat st W .cut (m,n) is trivial holds
not W is trivial
let W be Walk of G; :: thesis: for m, n being Nat st W .cut (m,n) is trivial holds
not W is trivial
let m, n be Nat; :: thesis: ( W .cut (m,n) is trivial implies not W is trivial )
assume that
A1: W .cut (m,n) is trivial and
A2: W is trivial ; :: thesis: contradiction
reconsider W = W as trivial Walk of G by A2;
reconsider m9 = m, n9 = n as Element of NAT by ORDINAL1:def 12;
W .cut (m9,n9) is trivial ;
hence contradiction by A1; :: thesis: verum