let C be _Graph; ( C is n + 3 -vertex & C is Cycle-like implies C is simple )
assume A1:
( C is n + 3 -vertex & C is Cycle-like )
; C is simple
assume A2:
not C is simple
; contradiction
C is (n + 1) + 2 -vertex
by A1;
then
not C is non-multi
by A1, A2;
then consider e1, e2, v1, v2 being object such that
A3:
( e1 Joins v1,v2,C & e2 Joins v1,v2,C & e1 <> e2 )
by GLIB_000:def 20;
A4:
e2 Joins v2,v1,C
by A3, GLIB_000:14;
set W1 = C .walkOf (v1,e1,v2);
set W2 = (C .walkOf (v1,e1,v2)) .addEdge e2;
A5:
(C .walkOf (v1,e1,v2)) .last() = v2
by A3, GLIB_001:15;
((C .walkOf (v1,e1,v2)) .addEdge e2) .first() =
(C .walkOf (v1,e1,v2)) .first()
by A4, A5, GLIB_001:63
.=
v1
by A3, GLIB_001:15
.=
((C .walkOf (v1,e1,v2)) .addEdge e2) .last()
by A4, A5, GLIB_001:63
;
then A6:
(C .walkOf (v1,e1,v2)) .addEdge e2 is closed
by GLIB_001:def 24;
A7: ((C .walkOf (v1,e1,v2)) .addEdge e2) .edgeSeq() =
((C .walkOf (v1,e1,v2)) .edgeSeq()) ^ <*e2*>
by A4, A5, GLIB_001:82
.=
<*e1*> ^ <*e2*>
by A3, GLIB_001:83
.=
<*e1,e2*>
by FINSEQ_1:def 9
;
then
((C .walkOf (v1,e1,v2)) .addEdge e2) .edgeSeq() is one-to-one
by A3, FINSEQ_3:94;
then A8:
(C .walkOf (v1,e1,v2)) .addEdge e2 is Trail-like
by GLIB_001:def 27;
len ((C .walkOf (v1,e1,v2)) .addEdge e2) =
(len (C .walkOf (v1,e1,v2))) + 2
by A4, A5, GLIB_001:64
.=
(len <*v1,e1,v2*>) + 2
by A3, GLIB_001:def 5
.=
3 + 2
by FINSEQ_1:45
;
then
(C .walkOf (v1,e1,v2)) .addEdge e2 is trivial
by GLIB_001:126;
then the_Edges_of C =
((C .walkOf (v1,e1,v2)) .addEdge e2) .edges()
by A1, A6, A8, Th39
.=
{e1,e2}
by A7, FINSEQ_2:127
;
then A9:
C .size() = 2
by A3, CARD_2:57;
A10:
C .size() = n + 3
by A1, GLIB_013:def 4;
n + 3 >= 0 + 3
by XREAL_1:6;
hence
contradiction
by A9, A10; verum