set D = (the_Vertices_of G) \/ (the_Edges_of G);

set X = { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 } ;

hence G .allTrails() is finite by FINSET_1:1, GRAPH_5:3; :: thesis: verum

set X = { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 } ;

A1: now :: thesis: for W being Trail of G holds len W <= (2 * (G .size())) + 1

let W be Trail of G; :: thesis: len W <= (2 * (G .size())) + 1

consider f being Function such that

A2: ( dom f = W .edgeSeq() & ( for x being object st x in W .edgeSeq() holds

f . x = x `2 ) ) from FUNCT_1:sch 3();

then Segm (card (W .edgeSeq())) c= Segm (card (the_Edges_of G)) by A2, A14, CARD_1:10;

then len (W .edgeSeq()) <= card (the_Edges_of G) by NAT_1:39;

then len (W .edgeSeq()) <= G .size() by GLIB_000:def 25;

then 2 * (len (W .edgeSeq())) <= 2 * (G .size()) by XREAL_1:64;

then (2 * (len (W .edgeSeq()))) + 1 <= (2 * (G .size())) + 1 by XREAL_1:7;

hence len W <= (2 * (G .size())) + 1 by Def15; :: thesis: verum

end;consider f being Function such that

A2: ( dom f = W .edgeSeq() & ( for x being object st x in W .edgeSeq() holds

f . x = x `2 ) ) from FUNCT_1:sch 3();

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds

x1 = x2

then A14:
f is one-to-one
by FUNCT_1:def 4;x1 = x2

A3:
W .edgeSeq() is one-to-one
by Def27;

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume that

A4: x1 in dom f and

A5: x2 in dom f and

A6: f . x1 = f . x2 ; :: thesis: x1 = x2

consider a1, b1 being object such that

A7: x1 = [a1,b1] by A2, A4, RELAT_1:def 1;

A8: a1 in dom (W .edgeSeq()) by A2, A4, A7, FUNCT_1:1;

A9: f . x2 = x2 `2 by A2, A5;

A10: (W .edgeSeq()) . a1 = b1 by A2, A4, A7, FUNCT_1:1;

consider a2, b2 being object such that

A11: x2 = [a2,b2] by A2, A5, RELAT_1:def 1;

A12: a2 in dom (W .edgeSeq()) by A2, A5, A11, FUNCT_1:1;

f . x1 = x1 `2 by A2, A4;

then A13: b1 = f . x1 by A7

.= b2 by A6, A9, A11 ;

then (W .edgeSeq()) . a2 = b1 by A2, A5, A11, FUNCT_1:1;

hence x1 = x2 by A7, A11, A13, A3, A8, A10, A12, FUNCT_1:def 4; :: thesis: verum

end;let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume that

A4: x1 in dom f and

A5: x2 in dom f and

A6: f . x1 = f . x2 ; :: thesis: x1 = x2

consider a1, b1 being object such that

A7: x1 = [a1,b1] by A2, A4, RELAT_1:def 1;

A8: a1 in dom (W .edgeSeq()) by A2, A4, A7, FUNCT_1:1;

A9: f . x2 = x2 `2 by A2, A5;

A10: (W .edgeSeq()) . a1 = b1 by A2, A4, A7, FUNCT_1:1;

consider a2, b2 being object such that

A11: x2 = [a2,b2] by A2, A5, RELAT_1:def 1;

A12: a2 in dom (W .edgeSeq()) by A2, A5, A11, FUNCT_1:1;

f . x1 = x1 `2 by A2, A4;

then A13: b1 = f . x1 by A7

.= b2 by A6, A9, A11 ;

then (W .edgeSeq()) . a2 = b1 by A2, A5, A11, FUNCT_1:1;

hence x1 = x2 by A7, A11, A13, A3, A8, A10, A12, FUNCT_1:def 4; :: thesis: verum

now :: thesis: for y being object st y in rng f holds

y in the_Edges_of G

then
rng f c= the_Edges_of G
by TARSKI:def 3;y in the_Edges_of G

let y be object ; :: thesis: ( y in rng f implies y in the_Edges_of G )

assume y in rng f ; :: thesis: y in the_Edges_of G

then consider x being object such that

A15: x in dom f and

A16: f . x = y by FUNCT_1:def 3;

consider a, b being object such that

A17: x = [a,b] by A2, A15, RELAT_1:def 1;

y = x `2 by A2, A15, A16;

then y = b by A17;

then y in rng (W .edgeSeq()) by A2, A15, A17, XTUPLE_0:def 13;

hence y in the_Edges_of G ; :: thesis: verum

end;assume y in rng f ; :: thesis: y in the_Edges_of G

then consider x being object such that

A15: x in dom f and

A16: f . x = y by FUNCT_1:def 3;

consider a, b being object such that

A17: x = [a,b] by A2, A15, RELAT_1:def 1;

y = x `2 by A2, A15, A16;

then y = b by A17;

then y in rng (W .edgeSeq()) by A2, A15, A17, XTUPLE_0:def 13;

hence y in the_Edges_of G ; :: thesis: verum

then Segm (card (W .edgeSeq())) c= Segm (card (the_Edges_of G)) by A2, A14, CARD_1:10;

then len (W .edgeSeq()) <= card (the_Edges_of G) by NAT_1:39;

then len (W .edgeSeq()) <= G .size() by GLIB_000:def 25;

then 2 * (len (W .edgeSeq())) <= 2 * (G .size()) by XREAL_1:64;

then (2 * (len (W .edgeSeq()))) + 1 <= (2 * (G .size())) + 1 by XREAL_1:7;

hence len W <= (2 * (G .size())) + 1 by Def15; :: thesis: verum

now :: thesis: for e being object st e in G .allTrails() holds

e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 }

then
G .allTrails() c= { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 }
by TARSKI:def 3;e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 }

let e be object ; :: thesis: ( e in G .allTrails() implies e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 } )

assume e in G .allTrails() ; :: thesis: e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 }

then consider W being Trail of G such that

A18: W = e ;

A19: len W <= (2 * (G .size())) + 1 by A1;

e is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * by A18, FINSEQ_1:def 11;

hence e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 } by A18, A19; :: thesis: verum

end;assume e in G .allTrails() ; :: thesis: e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 }

then consider W being Trail of G such that

A18: W = e ;

A19: len W <= (2 * (G .size())) + 1 by A1;

e is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * by A18, FINSEQ_1:def 11;

hence e in { x where x is Element of ((the_Vertices_of G) \/ (the_Edges_of G)) * : len x <= (2 * (G .size())) + 1 } by A18, A19; :: thesis: verum

hence G .allTrails() is finite by FINSET_1:1, GRAPH_5:3; :: thesis: verum