let G be connected finite Graph; ( ex p being Path of G st
( not p is cyclic & p is Eulerian ) iff ex v1, v2 being Vertex of G st
( v1 <> v2 & ( for v being Vertex of G holds
( Degree v is even iff ( v <> v1 & v <> v2 ) ) ) ) )
set V = the carrier of G;
set E = the carrier' of G;
given v1, v2 being Vertex of G such that A7:
v1 <> v2
and
A8:
for v being Vertex of G holds
( Degree v is even iff ( v <> v1 & v <> v2 ) )
; ex p being Path of G st
( not p is cyclic & p is Eulerian )
set G9 = AddNewEdge (v1,v2);
set E9 = the carrier' of (AddNewEdge (v1,v2));
A9:
the carrier' of (AddNewEdge (v1,v2)) = the carrier' of G \/ { the carrier' of G}
by Def7;
the carrier' of G in { the carrier' of G}
by TARSKI:def 1;
then A10:
the carrier' of G in the carrier' of (AddNewEdge (v1,v2))
by A9, XBOOLE_0:def 3;
A11:
the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) /\ the carrier' of G
by A9, XBOOLE_1:21;
for v being Vertex of (AddNewEdge (v1,v2)) holds Degree v is even
then consider P9 being cyclic Path of AddNewEdge (v1,v2) such that
A17:
P9 is Eulerian
by Th59;
A18:
rng P9 = the carrier' of (AddNewEdge (v1,v2))
by A17;
then consider n being Nat such that
A19:
n in dom P9
and
A20:
P9 . n = the carrier' of G
by A10, FINSEQ_2:10;
consider p9 being cyclic Path of AddNewEdge (v1,v2) such that
A21:
p9 . 1 = P9 . n
and
A22:
len p9 = len P9
and
A23:
rng p9 = rng P9
by A19, Th10;
reconsider p = ((1 + 1),(len p9)) -cut p9 as Path of AddNewEdge (v1,v2) by Th5;
consider vs9 being FinSequence of the carrier of (AddNewEdge (v1,v2)) such that
A24:
vs9 is_vertex_seq_of p9
by GRAPH_2:33;
A31:
( 1 <= n & n <= len P9 )
by A19, FINSEQ_3:25;
then A32:
1 <= len P9
by XXREAL_0:2;
then reconsider p1 = (1,1) -cut p9 as Chain of AddNewEdge (v1,v2) by A22, GRAPH_2:41;
A33:
p9 = p1 ^ (((1 + 1),(len p9)) -cut p9)
by A31, A22, FINSEQ_6:135, XXREAL_0:2;
reconsider vs = ((1 + 1),(len vs9)) -cut vs9 as FinSequence of the carrier of (AddNewEdge (v1,v2)) ;
A34:
len vs9 = (len p9) + 1
by A24;
now not len P9 = 1consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that A35:
not
c is
empty
and
vs is_vertex_seq_of c
and
vs . 1
= v1
and
vs . (len vs) = v2
by A7, Th18;
reconsider c =
c as
FinSequence of the
carrier' of
G by MSSCYC_1:def 1;
1
in dom c
by A35, FINSEQ_5:6;
then A36:
(
rng c c= the
carrier' of
G &
c . 1
in rng c )
by FINSEQ_1:def 4, FUNCT_1:def 3;
then A37:
c . 1
in the
carrier' of
G
;
c . 1
in the
carrier' of
(AddNewEdge (v1,v2))
by A9, A36, XBOOLE_0:def 3;
then consider m being
Nat such that A38:
m in dom P9
and A39:
P9 . m = c . 1
by A18, FINSEQ_2:10;
assume A40:
len P9 = 1
;
contradiction
( 1
<= m &
m <= len P9 )
by A38, FINSEQ_3:25;
then A41:
m = 1
by A40, XXREAL_0:1;
n = 1
by A31, A40, XXREAL_0:1;
hence
contradiction
by A20, A37, A39, A41;
verum end;
then
1 < len P9
by A32, XXREAL_0:1;
then A42:
1 + 1 <= len P9
by NAT_1:13;
then A43:
vs is_vertex_seq_of p
by A22, A24, GRAPH_2:42;
reconsider vs = vs as FinSequence of the carrier of G by Def7;
reconsider p = p as Path of G by A25, Th45;
take
p
; ( not p is cyclic & p is Eulerian )
A44:
( the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )
by Th34;
now not vs . 1 = vs . (len vs)
1
+ 1
<= (len p9) + 1
by A42, A22, NAT_1:12;
then A45:
1
+ 1
<= (len vs9) + 1
by A34, NAT_1:12;
then A46:
(len vs) + (1 + 1) = (len p9) + (1 + 1)
by A34, Lm1;
then
0 + 1
<= len vs
by A31, A22, XXREAL_0:2;
then consider i being
Nat such that
0 <= i
and A47:
i < len vs
and A48:
len vs = i + 1
by FINSEQ_6:127;
((len vs) + 1) + 1 =
(len vs) + (1 + 1)
.=
(len vs9) + 1
by A45, Lm1
;
then A49:
len vs9 = i + (1 + 1)
by A48;
A50:
vs9 . 1
= vs9 . (len vs9)
by A24, MSSCYC_1:6;
A51:
( (
vs9 . 1
= v1 &
vs9 . (1 + 1) = v2 ) or (
vs9 . 1
= v2 &
vs9 . (1 + 1) = v1 ) )
by A44, A20, A32, A21, A22, A24, Lm3;
assume A52:
vs . 1
= vs . (len vs)
;
contradiction
vs . (0 + 1) = vs9 . ((1 + 1) + 0)
by A31, A22, A45, A46, Lm1;
hence
contradiction
by A7, A52, A45, A47, A48, A49, A50, A51, Lm1;
verum
hence
not p is cyclic
by A43, A25, Th46, MSSCYC_1:6; p is Eulerian
( rng <* the carrier' of G*> = { the carrier' of G} & p1 = <* the carrier' of G*> )
by A20, A32, A21, A22, FINSEQ_1:39, FINSEQ_6:132;
then
( rng p9 = { the carrier' of G} \/ (rng p) & { the carrier' of G} misses rng p )
by A33, FINSEQ_1:31, FINSEQ_3:91;
hence
rng p = the carrier' of G
by A9, A18, A23, A1, XBOOLE_1:72; GRAPH_3:def 14 verum