let G be _finite non _trivial acyclic _Graph; ( the_Edges_of G <> {} implies ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 ) )
assume A1:
the_Edges_of G <> {}
; ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
defpred S1[ Nat] means ex W being Path of G st len W = $1;
set e = the Element of the_Edges_of G;
set src = (the_Source_of G) . the Element of the_Edges_of G;
set tar = (the_Target_of G) . the Element of the_Edges_of G;
the Element of the_Edges_of G Joins (the_Source_of G) . the Element of the_Edges_of G,(the_Target_of G) . the Element of the_Edges_of G,G
by A1, GLIB_000:def 13;
then A4:
len (G .walkOf (((the_Source_of G) . the Element of the_Edges_of G), the Element of the_Edges_of G,((the_Target_of G) . the Element of the_Edges_of G))) = 3
by GLIB_001:14;
then A5:
ex k being Nat st S1[k]
;
consider k being Nat such that
A6:
( S1[k] & ( for n being Nat st S1[n] holds
n <= k ) )
from NAT_1:sch 6(A2, A5);
consider W being Path of G such that
A7:
len W = k
and
A8:
for n being Nat st S1[n] holds
n <= k
by A6;
A9:
len (W .reverse()) = k
by A7, GLIB_001:21;
A10:
3 <= len W
by A4, A7, A8;
then A11:
W is V5()
by GLIB_001:125;
then A13:
W is open
by GLIB_001:def 24;
A14:
now for W being Path of G st len W = k & W is open holds
W .last() is endvertex let W be
Path of
G;
( len W = k & W is open implies W .last() is endvertex )assume that A15:
len W = k
and A16:
W is
open
;
W .last() is endvertex
2
+ 1
<= len W
by A4, A8, A15;
then
2
< len W
by NAT_1:13;
then reconsider lenW2 =
(len W) - (2 * 1) as
odd Element of
NAT by INT_1:5;
A17:
lenW2 + 2
= len W
;
A18:
W is
V5()
by A7, A10, A15, GLIB_001:125;
now W .last() is endvertex
W .last() in W .vertices()
by GLIB_001:88;
then
not
W .last() is
isolated
by A18, GLIB_001:135;
then
(W .last()) .degree() <> 0
by GLIB_000:def 50;
then
card ((W .last()) .edgesInOut()) <> 0
by GLIB_000:19;
then
0 < card ((W .last()) .edgesInOut())
by NAT_1:3;
then A19:
0 + 1
<= card ((W .last()) .edgesInOut())
by NAT_1:13;
assume
not
W .last() is
endvertex
;
contradictionthen
(W .last()) .degree() <> 1
by GLIB_000:def 52;
then
card ((W .last()) .edgesInOut()) <> 1
by GLIB_000:19;
then
1
< card ((W .last()) .edgesInOut())
by A19, XXREAL_0:1;
then consider e1,
e2 being
set such that A20:
e1 in (W .last()) .edgesInOut()
and A21:
(
e2 in (W .last()) .edgesInOut() &
e1 <> e2 )
by NAT_1:59;
then consider e being
set such that A24:
e in (W .last()) .edgesInOut()
and A25:
e <> W . (lenW2 + 1)
;
consider v being
Vertex of
G such that A26:
e Joins W .last() ,
v,
G
by A24, GLIB_000:64;
now contradictionper cases
( v in W .vertices() or not v in W .vertices() )
;
suppose
v in W .vertices()
;
contradictionthen consider n being
odd Element of
NAT such that A27:
n <= len W
and A28:
W . n = v
by GLIB_001:87;
set m =
W .rfind n;
set W2 =
W .cut (
(W .rfind n),
(len W));
A29:
W .rfind n <= len W
by A27, GLIB_001:def 22;
then
(W .cut ((W .rfind n),(len W))) .last() = W . (len W)
by GLIB_001:37;
then A30:
e Joins (W .cut ((W .rfind n),(len W))) .last() ,
v,
G
by A26, GLIB_001:def 7;
W . (W .rfind n) = v
by A27, A28, GLIB_001:def 22;
then A31:
(W .cut ((W .rfind n),(len W))) .first() = v
by A29, GLIB_001:37;
A32:
e in ((W .cut ((W .rfind n),(len W))) .last()) .edgesInOut()
by A30, GLIB_000:62;
now contradictionper cases
( not e in (W .cut ((W .rfind n),(len W))) .edges() or e in (W .cut ((W .rfind n),(len W))) .edges() )
;
suppose A33:
not
e in (W .cut ((W .rfind n),(len W))) .edges()
;
contradictionA34:
(W .cut ((W .rfind n),(len W))) .addEdge e is
V5()
by A30, GLIB_001:132;
(
((W .cut ((W .rfind n),(len W))) .addEdge e) .first() = v &
((W .cut ((W .rfind n),(len W))) .addEdge e) .last() = v )
by A31, A30, GLIB_001:63;
then A35:
(W .cut ((W .rfind n),(len W))) .addEdge e is
closed
by GLIB_001:def 24;
(W .cut ((W .rfind n),(len W))) .addEdge e is
Path-like
by A32, A33, Lm22;
then
(W .cut ((W .rfind n),(len W))) .addEdge e is
Cycle-like
by A35, A34, GLIB_001:def 31;
hence
contradiction
by Def2;
verum end; suppose A36:
e in (W .cut ((W .rfind n),(len W))) .edges()
;
contradiction
(W .cut ((W .rfind n),(len W))) .edges() c= W .edges()
by GLIB_001:106;
then consider a being
even Element of
NAT such that A37:
1
<= a
and A38:
a <= len W
and A39:
W . a = e
by A36, GLIB_001:99;
reconsider a1 =
a - 1 as
odd Element of
NAT by A37, INT_1:5;
A40:
a1 < (len W) - 0
by A38, XREAL_1:15;
a < lenW2 + 2
by A38, XXREAL_0:1;
then
a + 1
<= (lenW2 + 1) + 1
by NAT_1:13;
then
a <= lenW2 + 1
by XREAL_1:6;
then A41:
a < lenW2 + 1
by A25, A39, XXREAL_0:1;
a1 + 1
= a
;
then A42:
e Joins W . a1,
W . (a1 + 2),
G
by A39, A40, GLIB_001:def 3;
hence
contradiction
;
verum end; end; end; hence
contradiction
;
verum end; end; end; hence
contradiction
;
verum end; hence
W .last() is
endvertex
;
verum end;
W is_Walk_from W .first() ,W .last()
by GLIB_001:def 23;
then A47:
W .last() in G .reachableFrom (W .first())
by Def5;
W .reverse() is open
by A13, GLIB_001:120;
then
(W .reverse()) .last() is endvertex
by A14, A9;
then A48:
W .first() is endvertex
by GLIB_001:22;
W .last() is endvertex
by A7, A13, A14;
hence
ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
by A12, A48, A47; verum