let G be _Graph; :: thesis: for W1 being Trail of G st not W1 is trivial holds
ex W2 being Path of W1 st not W2 is trivial

let W1 be Trail of G; :: thesis: ( not W1 is trivial implies ex W2 being Path of W1 st not W2 is trivial )
assume not W1 is trivial ; :: thesis: not for W2 being Path of W1 holds W2 is trivial
then A1: 1 <> len W1 by Lm55;
1 <= len W1 by ABIAN:12;
then A2: 1 < len W1 by ;
now :: thesis: not for P being Path of W1 holds P is trivial
per cases ( W1 is open or W1 is closed ) ;
suppose A3: W1 is open ; :: thesis: not for P being Path of W1 holds P is trivial
set P = the Path of W1;
take P = the Path of W1; :: thesis: not P is trivial
A4: P .first() = W1 .first() by Th159;
A5: P .last() = W1 .last() by Th159;
W1 .first() <> W1 .last() by A3;
hence not P is trivial by A4, A5, Lm55; :: thesis: verum
end;
suppose A6: W1 is closed ; :: thesis: not for W2 being Path of W1 holds W2 is trivial
defpred S1[ Nat] means ( \$1 is odd & 1 < \$1 & \$1 <= len W1 & W1 . \$1 = W1 . (len W1) );
A7: ex k being Nat st S1[k] by A2;
consider k being Nat such that
A8: ( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from reconsider k = k as odd Element of NAT by ;
1 + 1 < k + 1 by ;
then 2 <= k by NAT_1:13;
then reconsider k2 = k - (2 * 1) as odd Element of NAT by INT_1:5;
set W3 = W1 .remove (k,(len W1));
set W4 = (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2);
set W5 = the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2);
consider es5 being Subset of (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()) such that
A9: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq() = Seq es5 by Def32;
A10: ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq() c= (W1 .remove (k,(len W1))) .edgeSeq() by Lm43;
W1 . k = W1 .last() by A8;
then A11: W1 .remove (k,(len W1)) = W1 .cut (1,k) by Th55;
then (W1 .remove (k,(len W1))) .edgeSeq() c= W1 .edgeSeq() by Lm43;
then ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq() c= W1 .edgeSeq() by ;
then reconsider es5 = es5 as Subset of () by XBOOLE_1:1;
A12: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is_Walk_from ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .first() ,((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .last() by Def32;
A13: (len (W1 .remove (k,(len W1)))) + (len W1) = (len W1) + k by ;
then A14: k2 <= (len (W1 .remove (k,(len W1)))) - 0 by XREAL_1:13;
A15: 1 <= k2 by ABIAN:12;
then ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .last() = (W1 .remove (k,(len W1))) . k2 by ;
then A16: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .last() = (W1 .remove (k,(len W1))) . k2 by A12;
k2 in dom (W1 .remove (k,(len W1))) by ;
then A17: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .last() = W1 . k2 by A8, A16, A11, Lm23;
((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .first() = (W1 .remove (k,(len W1))) . 1 by ;
then A18: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .first() = (W1 .remove (k,(len W1))) . 1 by A12;
A19: W1 . 1 = W1 . (len W1) by A6;
A20: now :: thesis: ( not the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is trivial implies not the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is closed )
1 <= len (W1 .remove (k,(len W1))) by ABIAN:12;
then A21: (2 * 0) + 1 in dom (W1 .remove (k,(len W1))) by FINSEQ_3:25;
assume that
A22: not the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is trivial and
A23: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is closed ; :: thesis: contradiction
the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .first() = W1 . k2 by ;
then A24: W1 . k2 = W1 . (len W1) by A19, A8, A18, A11, A21, Lm23;
now :: thesis: not k2 = 1
assume k2 = 1 ; :: thesis: contradiction
then len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) = 1 by ;
then A25: len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) <= 1 by Lm72;
1 <= len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) by ABIAN:12;
then len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) = 1 by ;
hence contradiction by A22, Lm55; :: thesis: verum
end;
then A26: 1 < k2 by ;
A27: k2 < k - 0 by XREAL_1:15;
then k2 <= len W1 by ;
hence contradiction by A8, A24, A26, A27; :: thesis: verum
end;
set e = W1 . (k2 + 1);
set W2 = the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .addEdge (W1 . (k2 + 1));
k2 < (len W1) - 0 by ;
then A28: W1 . (k2 + 1) Joins W1 . k2,W1 . (k2 + 2),G by Def3;
A29: k2 < (len (W1 .remove (k,(len W1)))) - 0 by ;
then A30: len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) = k2 by Lm22;
A31: now :: thesis: for m being odd Element of NAT st 1 < m & m <= len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) holds
the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . k
let m be odd Element of NAT ; :: thesis: ( 1 < m & m <= len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) implies the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . k )
assume that
A32: 1 < m and
A33: m <= len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) ; :: thesis: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . k
consider n being odd Element of NAT such that
A34: m <= n and
A35: n <= len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) and
A36: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m = ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) . n by ;
A37: 1 < n by ;
then n in dom ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) by ;
then A38: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m = (W1 .remove (k,(len W1))) . n by ;
A39: n + 0 < k2 + 2 by ;
then A40: n <= len W1 by ;
n in dom (W1 .remove (k,(len W1))) by ;
then the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m = W1 . n by A8, A11, A38, Lm23;
hence the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . m <> W1 . k by A8, A37, A39, A40; :: thesis: verum
end;
k2 + 1 <= k by ;
then A41: k2 + 1 <= len W1 by ;
now :: thesis: not W1 . (k2 + 1) in the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edges()
assume A42: W1 . (k2 + 1) in the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edges() ; :: thesis: contradiction
the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edges() c= ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edges() by Th161;
then consider n being even Element of NAT such that
A43: 1 <= n and
A44: n <= len ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) and
A45: ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) . n = W1 . (k2 + 1) by ;
A46: n < k2 + 1 by ;
n <= k2 + 2 by ;
then A47: n in dom (W1 .remove (k,(len W1))) by ;
n in dom ((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) by ;
then W1 . (k2 + 1) = (W1 .remove (k,(len W1))) . n by ;
then W1 . (k2 + 1) = W1 . n by A8, A11, A47, Lm23;
hence contradiction by A41, A43, A46, Lm57; :: thesis: verum
end;
then reconsider W2 = the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .addEdge (W1 . (k2 + 1)) as Path of G by ;
set g = ((k2 + 1) div 2) .--> (W1 . (k2 + 1));
set es = es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)));
A48: dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = (dom es5) \/ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) by FUNCT_4:def 1;
A50: (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . ((k2 + 1) div 2) = W1 . (k2 + 1) by FUNCOP_1:72;
A51: now :: thesis: for z being object st z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
z in W1 .edgeSeq()
let z be object ; :: thesis: ( z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies z in W1 .edgeSeq() )
assume A52: z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()
then consider x, y being object such that
A53: z = [x,y] by RELAT_1:def 1;
A54: x in dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) by ;
A55: y = (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) . x by ;
now :: thesis: z in W1 .edgeSeq()
per cases ( x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) or not x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ) ;
suppose A56: x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()
then A57: x = (k2 + 1) div 2 by TARSKI:def 1;
A58: 1 <= k2 + 1 by NAT_1:12;
then W1 . (k2 + 1) = () . x by ;
then A59: (W1 .edgeSeq()) . x = y by ;
x in dom () by ;
hence z in W1 .edgeSeq() by ; :: thesis: verum
end;
suppose A60: not x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()
then A61: x in dom es5 by ;
y = es5 . x by ;
then z in es5 by ;
hence z in W1 .edgeSeq() ; :: thesis: verum
end;
end;
end;
hence z in W1 .edgeSeq() ; :: thesis: verum
end;
then es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= W1 .edgeSeq() by TARSKI:def 3;
then dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) c= dom () by RELAT_1:11;
then A62: dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) c= Seg (len ()) by FINSEQ_1:def 3;
then reconsider es = es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) as FinSubsequence by FINSEQ_1:def 12;
reconsider es = es as Subset of () by ;
A63: dom es5 c= dom (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()) by FINSEQ_6:151;
now :: thesis: ( dom es5 c= Seg (len ()) & dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= Seg (len ()) & ( for x, y being Nat st x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
x < y ) )
thus ( dom es5 c= Seg (len ()) & dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= Seg (len ()) ) by ; :: thesis: for x, y being Nat st x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
x < y

let x, y be Nat; :: thesis: ( x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies x < y )
assume that
A64: x in dom es5 and
A65: y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: x < y
x <= len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()) by ;
then 2 * x <= 2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq())) by XREAL_1:64;
then (2 * x) + 1 <= (2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))) + 1 by XREAL_1:7;
then A66: (2 * x) + 1 <= k2 by ;
A67: 2 divides k2 + 1 by PEPIN:22;
y = (k2 + 1) div 2 by ;
then 2 * y = k2 + 1 by ;
then (2 * x) + 1 < 2 * y by ;
then A68: ((2 * x) + 1) - 1 < (2 * y) - 0 by XREAL_1:14;
then x <= y by XREAL_1:68;
hence x < y by ; :: thesis: verum
end;
then A69: Sgm (dom es) = (Sgm (dom es5)) ^ (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by ;
A70: k2 in dom (W1 .remove (k,(len W1))) by ;
then A71: the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .last() = W1 . k2 by A8, A16, A11, Lm23;
now :: thesis: ( len () = len (Seq es) & ( for x being Nat st 1 <= x & x <= len () holds
() . x = (Seq es) . x ) )
now :: thesis: not (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {}
assume (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {} ; :: thesis: contradiction
then consider x being object such that
A72: x in (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) by XBOOLE_0:def 1;
x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by A72;
then A73: x = (k2 + 1) div 2 by TARSKI:def 1;
x in dom es5 by ;
then (k2 + 1) div 2 <= len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()) by ;
then A74: 2 * ((k2 + 1) div 2) <= 2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq())) by XREAL_1:64;
2 divides k2 + 1 by PEPIN:22;
then k2 + 1 <= 2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq())) by ;
then (k2 + 1) + 1 <= (2 * (len (((W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) .edgeSeq()))) + 1 by XREAL_1:7;
then (1 + 1) + k2 <= 0 + k2 by ;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
then A75: dom es5 misses dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by XBOOLE_0:def 7;
len W2 = (len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 2 by ;
then A76: (len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 2 = (2 * (len ())) + 1 by Def15;
A77: len (Sgm (dom es5)) = card (dom es5) by
.= card es5 by CARD_1:62
.= len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) by ;
A78: now :: thesis: not (k2 + 1) div 2 = 0
assume (k2 + 1) div 2 = 0 ; :: thesis: contradiction
then A79: 2 * ((k2 + 1) div 2) = 2 * 0 ;
2 divides k2 + 1 by PEPIN:22;
hence contradiction by A79, NAT_D:3; :: thesis: verum
end;
A80: Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = <*((k2 + 1) div 2)*> by ;
then A81: len (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) = 1 by FINSEQ_1:40;
A82: (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) . 1 = (k2 + 1) div 2 by ;
set h = Sgm (dom es);
A83: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 14;
len (Seq es) = card es by Th4
.= card (dom es) by CARD_1:62 ;
then len (Seq es) = (card (dom es5)) + (card (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by
.= (card (dom es5)) + 1 by CARD_1:30
.= (card es5) + 1 by CARD_1:62
.= (len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq())) + 1 by ;
then A84: (2 * (len (Seq es))) + 1 = ((2 * (len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()))) + 1) + 2
.= (2 * (len ())) + 1 by ;
hence len () = len (Seq es) ; :: thesis: for x being Nat st 1 <= x & x <= len () holds
() . x = (Seq es) . x

let x be Nat; :: thesis: ( 1 <= x & x <= len () implies () . x = (Seq es) . x )
assume that
A85: 1 <= x and
A86: x <= len () ; :: thesis: () . x = (Seq es) . x
A87: dom es5 c= Seg (len ()) by ;
A88: x in dom (Seq es) by ;
then A89: (Sgm (dom es)) . x in dom es by ;
A90: dom (Sgm (dom es)) = Seg ((len (Sgm (dom es5))) + (len (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))))) by ;
A91: W1 . (k2 + 1) Joins the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .last() ,W1 . k,G by A8, A28, A16, A11, A70, Lm23;
A92: (Seq es) . x = es . ((Sgm (dom es)) . x) by ;
A93: x in dom (Sgm (dom es)) by ;
now :: thesis: (Seq es) . x = W2 . (2 * x)
per cases ( x <= len (Sgm (dom es5)) or len (Sgm (dom es5)) < x ) ;
suppose A94: x <= len (Sgm (dom es5)) ; :: thesis: (Seq es) . x = W2 . (2 * x)
then A95: x in dom (Sgm (dom es5)) by ;
then A96: (Sgm (dom es)) . x = (Sgm (dom es5)) . x by ;
rng (Sgm (dom es5)) = dom es5 by ;
then (Sgm (dom es)) . x in dom es5 by ;
then not (Sgm (dom es)) . x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by ;
then A97: (Seq es) . x = es5 . ((Sgm (dom es5)) . x) by ;
A98: x in dom ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) by ;
then A99: 2 * x in dom the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) by Lm41;
( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) . x = the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) . (2 * x) by ;
then A100: W2 . (2 * x) = ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()) . x by
.= (es5 * (Sgm (dom es5))) . x by ;
x in dom (es5 * (Sgm (dom es5))) by ;
hence (Seq es) . x = W2 . (2 * x) by ; :: thesis: verum
end;
suppose len (Sgm (dom es5)) < x ; :: thesis: (Seq es) . x = W2 . (2 * x)
then A101: (len (Sgm (dom es5))) + 1 <= x by NAT_1:13;
x <= (len (Sgm (dom es5))) + 1 by ;
then A102: x = (len (Sgm (dom es5))) + 1 by ;
1 in dom (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by ;
then A103: (Sgm (dom es)) . x = (k2 + 1) div 2 by ;
then (Sgm (dom es)) . x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by TARSKI:def 1;
then A104: (Seq es) . x = (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . ((k2 + 1) div 2) by
.= W1 . (k2 + 1) by FUNCOP_1:72
.= W2 . ((len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 1) by ;
2 * x = ((2 * (len ( the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .edgeSeq()))) + 1) + 1 by
.= (len the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2)) + 1 by Def15 ;
hence (Seq es) . x = W2 . (2 * x) by A104; :: thesis: verum
end;
end;
end;
hence (W2 .edgeSeq()) . x = (Seq es) . x by ; :: thesis: verum
end;
then A105: W2 .edgeSeq() = Seq es by FINSEQ_1:14;
1 <= len (W1 .remove (k,(len W1))) by ABIAN:12;
then (2 * 0) + 1 in dom (W1 .remove (k,(len W1))) by FINSEQ_3:25;
then the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) .first() = W1 .first() by A8, A18, A11, Lm23;
then the Path of (W1 .remove (k,(len W1))) .cut (((2 * 0) + 1),k2) is_Walk_from W1 .first() ,W1 . k2 by A71;
then W2 is_Walk_from W1 .first() ,W1 .last() by ;
then reconsider W2 = W2 as Path of W1 by ;
take W2 = W2; :: thesis: not W2 is trivial
thus not W2 is trivial by ; :: thesis: verum
end;
end;
end;
hence not for W2 being Path of W1 holds W2 is trivial ; :: thesis: verum