set D = () \/ ();
set X = { x where x is Element of (() \/ ()) * : len x <= (2 * ()) + 1 } ;
A1: now :: thesis: for W being Trail of G holds len W <= (2 * ()) + 1
let W be Trail of G; :: thesis: len W <= (2 * ()) + 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
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
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 ;
A8: a1 in dom () by ;
A9: f . x2 = x2 `2 by A2, A5;
A10: (W .edgeSeq()) . a1 = b1 by ;
consider a2, b2 being object such that
A11: x2 = [a2,b2] by ;
A12: a2 in dom () by ;
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 ;
hence x1 = x2 by ; :: thesis: verum
end;
then A14: f is one-to-one by FUNCT_1:def 4;
now :: thesis: for y being object st y in rng f holds
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:
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 ;
y = x `2 by A2, A15, A16;
then y = b by A17;
then y in rng () by ;
hence y in the_Edges_of G ; :: thesis: verum
end;
then rng f c= the_Edges_of G by TARSKI:def 3;
then Segm (card ()) c= Segm (card ()) by ;
then len () <= card () by NAT_1:39;
then len () <= G .size() by GLIB_000:def 25;
then 2 * (len ()) <= 2 * () by XREAL_1:64;
then (2 * (len ())) + 1 <= (2 * ()) + 1 by XREAL_1:7;
hence len W <= (2 * ()) + 1 by Def15; :: thesis: verum
end;
now :: thesis: for e being object st e in G .allTrails() holds
e in { x where x is Element of (() \/ ()) * : len x <= (2 * ()) + 1 }
let e be object ; :: thesis: ( e in G .allTrails() implies e in { x where x is Element of (() \/ ()) * : len x <= (2 * ()) + 1 } )
assume e in G .allTrails() ; :: thesis: e in { x where x is Element of (() \/ ()) * : len x <= (2 * ()) + 1 }
then consider W being Trail of G such that
A18: W = e ;
A19: len W <= (2 * ()) + 1 by A1;
e is Element of (() \/ ()) * by ;
hence e in { x where x is Element of (() \/ ()) * : len x <= (2 * ()) + 1 } by ; :: thesis: verum
end;
then G .allTrails() c= { x where x is Element of (() \/ ()) * : len x <= (2 * ()) + 1 } by TARSKI:def 3;
hence G .allTrails() is finite by ; :: thesis: verum