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 HEYTING3:1;
then A2: 1 < len W1 by A1, XXREAL_0:1;

now

per cases ( not W1 is closed or W1 is closed ) ;

suppose not W1 is closed ; :: thesis: not for P being Path of W1 holds P is trivial

then A3: W1 .first() <> W1 .last() by Def24;
consider P being Path of W1;
take P = P; :: thesis: not P is trivial
( P .first() = W1 .first() & P .last() = W1 .last() ) by Th162;
hence not P is trivial by A3, Lm55; :: thesis: verum

end;

suppose W1 is closed ; :: thesis: not for W2 being Path of W1 holds W2 is trivial

then A4: W1 . 1 = W1 . (len W1) by Th119;
defpred S₁[ Nat] means ( not $1 is even & 1 < $1 & $1 <= len W1 & W1 . $1 = W1 . (len W1) );
A5: ex k being Nat st S₁[k] by A2;
consider k being Nat such that
A6: ( S₁[k] & ( for m being Nat st S₁[m] holds
k <= m ) ) from NAT_1:sch 5(A5);
reconsider k = k as odd Element of NAT by A6, ORDINAL1:def 13;
set W3 = W1 .remove k,(len W1);
1 + 1 < k + 1 by A6, XREAL_1:10;
then 2 <= k by NAT_1:13;
then reconsider k2 = k - (2 * 1) as odd Element of NAT by INT_1:18;
set W4 = (W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2;
consider W5 being Path of (W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2;
set e = W1 . (k2 + 1);
set W2 = W5 .addEdge (W1 . (k2 + 1));
k2 < (len W1) - 0 by A6, XREAL_1:17;
then A7: W1 . (k2 + 1) Joins W1 . k2,W1 . (k2 + 2),G by Def3;
A8: (len (W1 .remove k,(len W1))) + (len W1) = (len W1) + k by A6, Lm24;
then A9: k2 <= (len (W1 .remove k,(len W1))) - 0 by XREAL_1:15;
A10: 1 <= k2 by HEYTING3:1;
then A11: ( ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .first() = (W1 .remove k,(len W1)) . 1 & ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .last() = (W1 .remove k,(len W1)) . k2 ) by A9, Lm16;
W5 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;
then A12: ( W5 .first() = (W1 .remove k,(len W1)) . 1 & W5 .last() = (W1 .remove k,(len W1)) . k2 ) by A11, Def23;
W1 . k = W1 .last() by A6;
then A13: W1 .remove k,(len W1) = W1 .cut 1,k by Th58;
k2 in dom (W1 .remove k,(len W1)) by A9, A10, FINSEQ_3:27;
then A14: W5 .last() = W1 . k2 by A6, A12, A13, Lm23;
A15: k2 < (len (W1 .remove k,(len W1))) - 0 by A8, XREAL_1:17;
then k2 + 1 <= k by A8, NAT_1:13;
then A16: k2 + 1 <= len W1 by A6, XXREAL_0:2;
A17: len ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) = k2 by A15, Lm22;

A18: now

assume A19: W1 . (k2 + 1) in W5 .edges() ; :: thesis: contradiction
W5 .edges() c= ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edges() by Th164;
then consider n being even Element of NAT such that
A20: ( 1 <= n & n <= len ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) & ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) . n = W1 . (k2 + 1) ) by A19, Lm46;
n in dom ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) by A20, FINSEQ_3:27;
then A21: W1 . (k2 + 1) = (W1 .remove k,(len W1)) . n by A9, A20, Lm23;
n <= k2 + 2 by A17, A20, NAT_1:12;
then n in dom (W1 .remove k,(len W1)) by A8, A20, FINSEQ_3:27;
then A22: W1 . (k2 + 1) = W1 . n by A6, A13, A21, Lm23;
n < k2 + 1 by A17, A20, NAT_1:13;
hence contradiction by A16, A20, A22, Lm57; :: thesis: verum

end;

A23: now

assume A24: ( not W5 is trivial & W5 is closed ) ; :: thesis: contradiction
then A25: W5 .first() = W1 . k2 by A14, Def24;
1 <= len (W1 .remove k,(len W1)) by HEYTING3:1;
then (2 * 0 ) + 1 in dom (W1 .remove k,(len W1)) by FINSEQ_3:27;
then A26: W1 . k2 = W1 . (len W1) by A4, A6, A12, A13, A25, Lm23;

now

assume k2 = 1 ; :: thesis: contradiction
then len ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) = 1 by A9, Lm22;
then ( 1 <= len W5 & len W5 <= 1 ) by Lm72, HEYTING3:1;
then len W5 = 1 by XXREAL_0:1;
hence contradiction by A24, Lm55; :: thesis: verum

end;

then A27: 1 < k2 by A10, XXREAL_0:1;
A28: k2 < k - 0 by XREAL_1:17;
then k2 <= len W1 by A6, XXREAL_0:2;
hence contradiction by A6, A26, A27, A28; :: thesis: verum

end;

now

let m be odd Element of NAT ; :: thesis: ( 1 < m & m <= len W5 implies W5 . m <> W1 . k )
assume A29: ( 1 < m & m <= len W5 ) ; :: thesis: W5 . m <> W1 . k
then consider n being odd Element of NAT such that
A30: ( m <= n & n <= len ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) & W5 . m = ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) . n ) by Th165;
A31: 1 < n by A29, A30, XXREAL_0:2;
then n in dom ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) by A30, FINSEQ_3:27;
then A32: W5 . m = (W1 .remove k,(len W1)) . n by A9, A30, Lm23;
A33: n + 0 < k2 + 2 by A17, A30, XREAL_1:10;
then n in dom (W1 .remove k,(len W1)) by A8, A31, FINSEQ_3:27;
then A34: W5 . m = W1 . n by A6, A13, A32, Lm23;
n <= len W1 by A6, A33, XXREAL_0:2;
hence W5 . m <> W1 . k by A6, A31, A33, A34; :: thesis: verum

end;

then reconsider W2 = W5 .addEdge (W1 . (k2 + 1)) as Path of G by A7, A14, A18, A23, Th151;
1 <= len (W1 .remove k,(len W1)) by HEYTING3:1;
then (2 * 0 ) + 1 in dom (W1 .remove k,(len W1)) by FINSEQ_3:27;
then A35: W5 .first() = W1 .first() by A6, A12, A13, Lm23;
A36: k2 in dom (W1 .remove k,(len W1)) by A10, A15, FINSEQ_3:27;
then A37: W5 .last() = W1 . k2 by A6, A12, A13, Lm23;
then W5 is_Walk_from W1 .first() ,W1 . k2 by A35, Def23;
then A38: W2 is_Walk_from W1 .first() ,W1 .last() by A6, A7, Lm39;
consider es5 being Subset of (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() ) such that
A39: W5 .edgeSeq() = Seq es5 by Def32;
A40: ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() c= (W1 .remove k,(len W1)) .edgeSeq() by Lm43;
(W1 .remove k,(len W1)) .edgeSeq() c= W1 .edgeSeq() by A13, Lm43;
then ((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() c= W1 .edgeSeq() by A40, XBOOLE_1:1;
then reconsider es5 = es5 as Subset of (W1 .edgeSeq() ) by XBOOLE_1:1;
set g = ((k2 + 1) div 2) .--> (W1 . (k2 + 1));
set es = es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)));
A41: ( dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = (dom es5) \/ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) & ( for x being set st x in (dom es5) \/ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) holds
( ( x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) . x = (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . x ) & ( not x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) . x = es5 . x ) ) ) ) by FUNCT_4:def 1;
A42: ( dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) = {((k2 + 1) div 2)} & rng (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) = {(W1 . (k2 + 1))} ) by FUNCOP_1:14, FUNCOP_1:19;
A43: (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . ((k2 + 1) div 2) = W1 . (k2 + 1) by FUNCOP_1:87;

A44: now

let z be set ; :: thesis: ( z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies z in W1 .edgeSeq() )
assume A45: z in es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()
then consider x, y being set such that
A46: z = [x,y] by RELAT_1:def 1;
A47: ( x in dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) & y = (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) . x ) by A45, A46, FUNCT_1:8;

now

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 A48: x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()

then A49: x = (k2 + 1) div 2 by A42, TARSKI:def 1;
1 <= k2 + 1 by NAT_1:12;
then A50: ( x in dom (W1 .edgeSeq() ) & W1 . (k2 + 1) = (W1 .edgeSeq() ) . x ) by A16, A49, Lm40;
then (W1 .edgeSeq() ) . x = y by A41, A43, A47, A48, A49;
hence z in W1 .edgeSeq() by A46, A50, FUNCT_1:8; :: thesis: verum

end;

suppose A51: not x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ; :: thesis: z in W1 .edgeSeq()

then A52: x in dom es5 by A41, A47, XBOOLE_0:def 3;
y = es5 . x by A41, A47, A51;
then z in es5 by A46, A52, FUNCT_1:8;
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 (W1 .edgeSeq() ) by RELAT_1:25;
then A53: dom (es5 +* (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) c= Seg (len (W1 .edgeSeq() )) 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 (W1 .edgeSeq() ) by A44, TARSKI:def 3;
A54: dom es5 c= dom (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() ) by GRAPH_2:27;

now

thus ( dom es5 c= Seg (len (W1 .edgeSeq() )) & dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) c= Seg (len (W1 .edgeSeq() )) ) by A41, A53, XBOOLE_1:11; :: thesis: for x, y being Element of NAT st x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) holds
x < y
let x, y be Element of NAT ; :: thesis: ( x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) implies x < y )
assume A55: ( x in dom es5 & y in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ) ; :: thesis: x < y
A56: y = (k2 + 1) div 2 by A42, A55, TARSKI:def 1;
2 divides k2 + 1 by PEPIN:22;
then A57: 2 * y = k2 + 1 by A56, NAT_D:3;
x <= len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() ) by A54, A55, FINSEQ_3:27;
then 2 * x <= 2 * (len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() )) by XREAL_1:66;
then (2 * x) + 1 <= (2 * (len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() ))) + 1 by XREAL_1:9;
then (2 * x) + 1 <= k2 by A17, Def15;
then (2 * x) + 1 < 2 * y by A57, NAT_1:13;
then A58: ((2 * x) + 1) - 1 < (2 * y) - 0 by XREAL_1:16;
then x <= y by XREAL_1:70;
hence x < y by A58, XXREAL_0:1; :: thesis: verum

end;

then A59: Sgm (dom es) = (Sgm (dom es5)) ^ (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by A41, FINSEQ_3:48;

now

A60: W1 . (k2 + 1) Joins W5 .last() ,W1 . k,G by A6, A7, A12, A13, A36, Lm23;
len W2 = (len W5) + 2 by A7, A37, Lm37;
then A61: (len W5) + 2 = (2 * (len (W2 .edgeSeq() ))) + 1 by Def15;
A62: len (Seq es) = card es by Th5
.= card (dom es) by CARD_1:104 ;

now

assume (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) <> {} ; :: thesis: contradiction
then consider x being set such that
A63: x in (dom es5) /\ (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) by XBOOLE_0:def 1;
A64: ( x in dom es5 & x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) ) by A63, XBOOLE_0:def 4;
then x = (k2 + 1) div 2 by A42, TARSKI:def 1;
then (k2 + 1) div 2 <= len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() ) by A54, A64, FINSEQ_3:27;
then A65: 2 * ((k2 + 1) div 2) <= 2 * (len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() )) by XREAL_1:66;
2 divides k2 + 1 by PEPIN:22;
then k2 + 1 <= 2 * (len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() )) by A65, NAT_D:3;
then (k2 + 1) + 1 <= (2 * (len (((W1 .remove k,(len W1)) .cut ((2 * 0 ) + 1),k2) .edgeSeq() ))) + 1 by XREAL_1:9;
then (1 + 1) + k2 <= 0 + k2 by A17, Def15;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then A66: dom es5 misses dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by XBOOLE_0:def 7;
then len (Seq es) = (card (dom es5)) + (card (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by A41, A62, CARD_2:53
.= (card (dom es5)) + 1 by A42, CARD_1:50
.= (card es5) + 1 by CARD_1:104
.= (len (W5 .edgeSeq() )) + 1 by A39, Th5 ;
then A67: (2 * (len (Seq es))) + 1 = ((2 * (len (W5 .edgeSeq() ))) + 1) + 2
.= (2 * (len (W2 .edgeSeq() ))) + 1 by A61, Def15 ;
hence len (W2 .edgeSeq() ) = len (Seq es) ; :: thesis: for x being Nat st 1 <= x & x <= len (W2 .edgeSeq() ) holds
(W2 .edgeSeq() ) . x = (Seq es) . x
let x be Nat; :: thesis: ( 1 <= x & x <= len (W2 .edgeSeq() ) implies (W2 .edgeSeq() ) . x = (Seq es) . x )
assume A68: ( 1 <= x & x <= len (W2 .edgeSeq() ) ) ; :: thesis: (W2 .edgeSeq() ) . x = (Seq es) . x
set h = Sgm (dom es);
A69: Seq es = es * (Sgm (dom es)) by FINSEQ_1:def 14;
A70: x in dom (Seq es) by A67, A68, FINSEQ_3:27;
then A71: ( x in dom (Sgm (dom es)) & (Sgm (dom es)) . x in dom es ) by A69, FUNCT_1:21;
A72: (Seq es) . x = es . ((Sgm (dom es)) . x) by A69, A70, FUNCT_1:22;
A73: ( dom (Sgm (dom es)) = Seg ((len (Sgm (dom es5))) + (len (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))))) & ( for x being Element of NAT st x in dom (Sgm (dom es5)) holds
(Sgm (dom es)) . x = (Sgm (dom es5)) . x ) & ( for x being Element of NAT st x in dom (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) holds
(Sgm (dom es)) . ((len (Sgm (dom es5))) + x) = (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) . x ) ) by A59, FINSEQ_1:def 7;
A74: Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = Sgm {((k2 + 1) div 2)} by FUNCOP_1:19;

now

assume (k2 + 1) div 2 = 0 ; :: thesis: contradiction
then A75: 2 * ((k2 + 1) div 2) = 2 * 0 ;
2 divides k2 + 1 by PEPIN:22;
hence contradiction by A75, NAT_D:3; :: thesis: verum

end;

then Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1)))) = <*((k2 + 1) div 2)*> by A74, FINSEQ_3:50;
then A76: ( len (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) = 1 & (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) . 1 = (k2 + 1) div 2 ) by FINSEQ_1:57;
A77: dom es5 c= Seg (len (W1 .edgeSeq() )) by A41, A53, XBOOLE_1:11;
then A78: len (Sgm (dom es5)) = card (dom es5) by FINSEQ_3:44
.= card es5 by CARD_1:104
.= len (W5 .edgeSeq() ) by A39, Th5 ;

now

per cases ( x <= len (Sgm (dom es5)) or len (Sgm (dom es5)) < x ) ;

suppose A79: x <= len (Sgm (dom es5)) ; :: thesis: (Seq es) . x = W2 . (2 * x)

then A80: x in dom (Sgm (dom es5)) by A68, FINSEQ_3:27;
then A81: (Sgm (dom es)) . x = (Sgm (dom es5)) . x by A59, FINSEQ_1:def 7;
rng (Sgm (dom es5)) = dom es5 by A77, FINSEQ_1:def 13;
then (Sgm (dom es)) . x in dom es5 by A80, A81, FUNCT_1:def 5;
then not (Sgm (dom es)) . x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by A66, XBOOLE_0:3;
then A82: (Seq es) . x = es5 . ((Sgm (dom es5)) . x) by A41, A71, A72, A81;
A83: (W5 .edgeSeq() ) . x = W5 . (2 * x) by A68, A78, A79, Def15;
A84: x in dom (W5 .edgeSeq() ) by A68, A78, A79, FINSEQ_3:27;
then 2 * x in dom W5 by Lm41;
then A85: W2 . (2 * x) = (W5 .edgeSeq() ) . x by A60, A83, Lm38
.= (es5 * (Sgm (dom es5))) . x by A39, FINSEQ_1:def 14 ;
x in dom (es5 * (Sgm (dom es5))) by A39, A84, FINSEQ_1:def 14;
hence (Seq es) . x = W2 . (2 * x) by A82, A85, FUNCT_1:22; :: thesis: verum

end;

suppose len (Sgm (dom es5)) < x ; :: thesis: (Seq es) . x = W2 . (2 * x)

then A86: (len (Sgm (dom es5))) + 1 <= x by NAT_1:13;
x <= (len (Sgm (dom es5))) + 1 by A71, A73, A76, FINSEQ_1:3;
then A87: x = (len (Sgm (dom es5))) + 1 by A86, XXREAL_0:1;
1 in dom (Sgm (dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))))) by A76, FINSEQ_3:27;
then A88: (Sgm (dom es)) . x = (k2 + 1) div 2 by A59, A76, A87, FINSEQ_1:def 7;
then (Sgm (dom es)) . x in dom (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) by A42, TARSKI:def 1;
then A89: (Seq es) . x = (((k2 + 1) div 2) .--> (W1 . (k2 + 1))) . ((k2 + 1) div 2) by A41, A71, A72, A88
.= W1 . (k2 + 1) by FUNCOP_1:87
.= W2 . ((len W5) + 1) by A60, Lm38 ;
2 * x = ((2 * (len (W5 .edgeSeq() ))) + 1) + 1 by A78, A87
.= (len W5) + 1 by Def15 ;
hence (Seq es) . x = W2 . (2 * x) by A89; :: thesis: verum

end;

end;

end;

hence (W2 .edgeSeq() ) . x = (Seq es) . x by A68, Def15; :: thesis: verum

end;

then W2 .edgeSeq() = Seq es by FINSEQ_1:18;
then reconsider W2 = W2 as Path of W1 by A38, Def32;
take W2 = W2; :: thesis: not W2 is trivial
thus not W2 is trivial by A7, A14, Th133; :: thesis: verum

end;

end;

end;

hence not for W2 being Path of W1 holds W2 is trivial ; :: thesis: verum