let C be Cycle-like _Graph; ( C .order() = 2 iff not C is non-multi )
hereby ( not C is non-multi implies C .order() = 2 )
assume A1:
C .order() = 2
;
not C is non-multi then A2:
not
C is
_trivial
by GLIB_000:26;
consider v1,
v2 being
object such that A3:
(
v1 <> v2 &
the_Vertices_of C = {v1,v2} )
by A1, CARD_2:60;
reconsider v1 =
v1,
v2 =
v2 as
Vertex of
C by A3, TARSKI:def 2;
2 =
v1 .degree()
by GLIB_016:def 4
.=
card (v1 .edgesInOut())
by A2, GLIB_000:19
;
then consider e1,
e2 being
object such that A4:
(
e1 <> e2 &
v1 .edgesInOut() = {e1,e2} )
by CARD_2:60;
e1 in v1 .edgesInOut()
by A4, TARSKI:def 2;
then consider w1 being
Vertex of
C such that A5:
e1 Joins v1,
w1,
C
by GLIB_000:64;
e2 in v1 .edgesInOut()
by A4, TARSKI:def 2;
then consider w2 being
Vertex of
C such that A6:
e2 Joins v1,
w2,
C
by GLIB_000:64;
(
v1 <> w1 &
v1 <> w2 )
by A2, A5, A6, GLIB_000:18;
then
(
w1 = v2 &
w2 = v2 )
by A3, TARSKI:def 2;
hence
not
C is
non-multi
by A4, A5, A6, GLIB_000:def 20;
verum
end;
assume
not C is non-multi
; C .order() = 2
then consider e1, e2, v1, v2 being object such that
A7:
( e1 Joins v1,v2,C & e2 Joins v1,v2,C & e1 <> e2 )
by GLIB_000:def 20;
reconsider v1 = v1, v2 = v2 as Vertex of C by A7, GLIB_000:13;
reconsider e1 = e1, e2 = e2 as set by TARSKI:1;
set W1 = C .walkOf (v1,e1,v2);
set W2 = (C .walkOf (v1,e1,v2)) .addEdge e2;
A8:
( (C .walkOf (v1,e1,v2)) .first() = v1 & (C .walkOf (v1,e1,v2)) .last() = v2 )
by A7, GLIB_001:15;
then A9:
e2 Joins (C .walkOf (v1,e1,v2)) .last() ,v1,C
by A7, GLIB_000:14;
then A10:
(C .walkOf (v1,e1,v2)) .addEdge e2 is closed
by A8, GLIB_001:63, GLIB_001:119;
len (C .walkOf (v1,e1,v2)) = 3
by A7, GLIB_001:14;
then A11:
len ((C .walkOf (v1,e1,v2)) .addEdge e2) = 3 + 2
by A9, GLIB_001:64;
then A12:
(C .walkOf (v1,e1,v2)) .addEdge e2 is trivial
by GLIB_001:126;
((C .walkOf (v1,e1,v2)) .addEdge e2) .edgeSeq() =
((C .walkOf (v1,e1,v2)) .edgeSeq()) ^ <*e2*>
by A9, GLIB_001:82
.=
<*e1*> ^ <*e2*>
by A7, GLIB_001:83
.=
<*e1,e2*>
by FINSEQ_1:def 9
;
then
((C .walkOf (v1,e1,v2)) .addEdge e2) .edgeSeq() is one-to-one
by A7, FINSEQ_3:94;
then A13:
(C .walkOf (v1,e1,v2)) .addEdge e2 is Trail-like
by GLIB_001:def 27;
A14:
v1 <> v2
proof
assume
v1 = v2
;
contradiction
then A15:
(
e1 DJoins v1,
v1,
C &
e2 DJoins v1,
v1,
C )
by A7, GLIB_000:16;
then
(
e1 in v1 .edgesIn() &
e2 in v1 .edgesIn() )
by GLIB_000:57;
then
card {e1,e2} c= v1 .inDegree()
by CARD_1:11, ZFMISC_1:32;
then A16:
2
c= v1 .inDegree()
by A7, CARD_2:57;
{e1} c= v1 .edgesOut()
by A15, GLIB_000:59, ZFMISC_1:31;
then
card {e1} c= v1 .outDegree()
by CARD_1:11;
then
1
c= v1 .outDegree()
by CARD_1:30;
then
2
+` 1
c= v1 .degree()
by A16, CARD_2:83;
then A17:
3
c= 2
by GLIB_016:def 4;
2
in {0,1,2}
by ENUMSET1:def 1;
then
2
in 2
by A17, CARD_1:51;
hence
contradiction
;
verum
end;
now for m, n being odd Element of NAT st m < n & n <= len ((C .walkOf (v1,e1,v2)) .addEdge e2) & ((C .walkOf (v1,e1,v2)) .addEdge e2) . m = ((C .walkOf (v1,e1,v2)) .addEdge e2) . n holds
( not m <> 1 & not n <> len ((C .walkOf (v1,e1,v2)) .addEdge e2) )let m,
n be
odd Element of
NAT ;
( m < n & n <= len ((C .walkOf (v1,e1,v2)) .addEdge e2) & ((C .walkOf (v1,e1,v2)) .addEdge e2) . m = ((C .walkOf (v1,e1,v2)) .addEdge e2) . n implies ( not m <> 1 & not n <> len ((C .walkOf (v1,e1,v2)) .addEdge e2) ) )A18:
(C .walkOf (v1,e1,v2)) .addEdge e2 =
(C .walkOf (v1,e1,v2)) ^ <*e2,v1*>
by A9, GLIB_001:62
.=
<*v1,e1,v2*> ^ <*e2,v1*>
by A7, GLIB_001:def 5
.=
<*v1,e1,v2,e2,v1*>
by FINSEQ_4:75
;
assume A19:
(
m < n &
n <= len ((C .walkOf (v1,e1,v2)) .addEdge e2) &
((C .walkOf (v1,e1,v2)) .addEdge e2) . m = ((C .walkOf (v1,e1,v2)) .addEdge e2) . n )
;
( not m <> 1 & not n <> len ((C .walkOf (v1,e1,v2)) .addEdge e2) )assume
(
m <> 1 or
n <> len ((C .walkOf (v1,e1,v2)) .addEdge e2) )
;
contradictionper cases then
( m <> 1 or n <> len ((C .walkOf (v1,e1,v2)) .addEdge e2) )
;
suppose A20:
m <> 1
;
contradiction
m < 4
+ 1
by A11, A19, XXREAL_0:2;
then A21:
m = 3
by A20, NAT_1:13, CHORD:7;
n + 0 <= 5
+ 1
by A11, A19, XREAL_1:7;
then
(
n = 1 or
n = 3 or
n = 5 )
by CHORD:8;
then
(
((C .walkOf (v1,e1,v2)) .addEdge e2) . m = v2 &
((C .walkOf (v1,e1,v2)) .addEdge e2) . n = v1 )
by A18, A19, A21, FINSEQ_4:78;
hence
contradiction
by A14, A19;
verum end; suppose
n <> len ((C .walkOf (v1,e1,v2)) .addEdge e2)
;
contradictionthen
n < 4
+ 1
by A11, A19, XXREAL_0:1;
then A22:
n <= 4
by NAT_1:13;
1
<= m
by CHORD:2;
then A23:
n = 3
by A19, A22, CHORD:7;
then
m < 2
+ 1
by A19;
then
m = 1
by CHORD:6, NAT_1:13;
then
(
((C .walkOf (v1,e1,v2)) .addEdge e2) . m = v1 &
((C .walkOf (v1,e1,v2)) .addEdge e2) . n = v2 )
by A18, A23, FINSEQ_4:78;
hence
contradiction
by A14, A19;
verum end; end;
then
(C .walkOf (v1,e1,v2)) .addEdge e2 is Path-like
by A13, GLIB_001:def 28;
then the_Vertices_of C =
((C .walkOf (v1,e1,v2)) .addEdge e2) .vertices()
by A10, A12, Th39
.=
((C .walkOf (v1,e1,v2)) .vertices()) \/ {v1}
by A9, GLIB_001:95
.=
{v1} \/ {v1,v2}
by A7, GLIB_001:91
.=
{v1,v1,v2}
by ENUMSET1:2
.=
{v1,v2}
by ENUMSET1:30
;
hence
C .order() = 2
by A14, CARD_2:57; verum