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