for g1, g2 being Vertex of KoenigsbergBridges st g1 <> g2 holds
ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 )

proof

let g1, g2 be Vertex of KoenigsbergBridges; :: thesis:
assume g: g1 <> g2 ; :: thesis:

per cases by ENUMSET1:def 2;

suppose ( g1 = 0 & g2 = 0 ) ; :: thesis:

hence ex c being Chain of KoenigsbergBridges ex vs being FinSequence of the carrier of KoenigsbergBridges st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = g1 & vs . (len vs) = g2 ) by g; :: thesis:

end;

suppose gg: ( g1 = 0 & g2 = 1 ) ; :: thesis:

10 in KEdges by ENUMSET1:def 5;
then reconsider c = <*10*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c ; :: thesis:
reconsider vs = <*g1,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not c is empty ; :: thesis:
l: ( len c = 1 & c . 1 = 10 ) by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 10 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [10,0] in KSource & [10,1] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g1 & KTarget . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 0 & g2 = 2 ) ; :: thesis:

20 in KEdges by ENUMSET1:def 5;
then reconsider c = <*20*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c ; :: thesis:
reconsider vs = <*g1,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not c is empty ; :: thesis:
l: ( len c = 1 & c . 1 = 20 ) by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 20 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [20,0] in KSource & [20,2] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g1 & KTarget . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 0 & g2 = 3 ) ; :: thesis:

30 in KEdges by ENUMSET1:def 5;
then reconsider c = <*30*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c ; :: thesis:
reconsider vs = <*g1,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not c is empty ; :: thesis:
l: ( len c = 1 & c . 1 = 30 ) by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 30 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [30,0] in KSource & [30,3] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g1 & KTarget . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 1 & g2 = 0 ) ; :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 10 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [10,0] in KSource & [10,1] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g2 & KTarget . (c . n) = g1 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose ( g1 = 1 & g2 = 1 ) ; :: thesis:

end;

suppose gg: ( g1 = 1 & g2 = 2 ) ; :: thesis:

40 in KEdges by ENUMSET1:def 5;
then reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c ; :: thesis:
reconsider vs = <*g1,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not c is empty ; :: thesis:
l: ( len c = 1 & c . 1 = 40 ) by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 40 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [40,1] in KSource & [40,2] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g1 & KTarget . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 1 & g2 = 3 ) ; :: thesis:

reconsider g3 = 2 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
40 in KEdges by ENUMSET1:def 5;
then reconsider c = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
60 in KEdges by ENUMSET1:def 5;
then reconsider d = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
reconsider vs1 = <*g1,g3*> as FinSequence of the carrier of KoenigsbergBridges ;
l: ( len c = 1 & c . 1 = 40 ) by FINSEQ_1:40;
lv1: len vs1 = 2 by FINSEQ_1:44;
vs1: vs1 is_vertex_seq_of c

proof

thus len vs1 = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 40 ;
dom vs1 = Seg 2 by lv1, FINSEQ_1:def 3;
then dom vs1 = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs1 & 2 in dom vs1 ) by TARSKI:def 2;
v1: vs1 /. n = vs1 . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs1 /. (n + 1) = vs1 . 2 by d, n, PARTFUN1:def 6
.= g3 ;
( [40,1] in KSource & [40,2] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g1 & KTarget . (c . n) = g3 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs1 /. n,vs1 /. (n + 1) by v1, v2; :: thesis:

end;

reconsider vs2 = <*g3,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
l: ( len d = 1 & d . 1 = 60 ) by FINSEQ_1:40;
lv: len vs2 = 2 by FINSEQ_1:44;
vs2: vs2 is_vertex_seq_of d

proof

thus len vs2 = (len d) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len d ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: d . n = 60 ;
dom vs2 = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs2 = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs2 & 2 in dom vs2 ) by TARSKI:def 2;
v1: vs2 /. n = vs2 . n by d, n, PARTFUN1:def 6
.= g3 by n ;
v2: vs2 /. (n + 1) = vs2 . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [60,2] in KSource & [60,3] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (d . n) = g3 & KTarget . (d . n) = g2 ) by cn, gg, FUNCT_1:1;
hence d . n joins vs2 /. n,vs2 /. (n + 1) by v1, v2; :: thesis:

end;

( rng c = {40} & rng d = {60} ) by FINSEQ_1:38;
then r: rng c misses rng d by ZFMISC_1:11;
vs1 . (len vs1) = g3 by lv1
.= vs2 . 1 ;
then reconsider cd = c ^ d as Path of KoenigsbergBridges by vs1, vs2, r, GRAPH_3:6;
take cd ; :: thesis:
reconsider vs = <*g1,g3,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not cd is empty ; :: thesis:
cd = <*40,60*> ;
then l: ( len cd = 2 & cd . 1 = 40 & cd . 2 = 60 ) by FINSEQ_1:44;
lv: len vs = 3 by FINSEQ_1:45;
thus vs is_vertex_seq_of cd :: thesis:

proof

thus len vs = (len cd) + 1 by l, FINSEQ_1:45; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len cd ) ; :: thesis:
then ( 1 <= n & n <= 1 + 1 ) by l;
then not not n = 1 + 0 & ... & not n = 1 + 1 by NAT_1:62;
then ( n = 1 or n = 2 ) ;

per cases ;

suppose n: n = 1 ; :: thesis:

then cn: cd . n = 40 by l;
dom vs = Seg 3 by lv, FINSEQ_1:def 3;
then dom vs = {1,2,3} by FINSEQ_3:1;
then d: ( 1 in dom vs & 2 in dom vs ) by ENUMSET1:def 1;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g3 ;
( [40,1] in KSource & [40,2] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (cd . n) = g1 & KTarget . (cd . n) = g3 ) by cn, gg, FUNCT_1:1;
hence cd . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

suppose n: n = 2 ; :: thesis:

then cn: cd . n = 60 by l;
dom vs = Seg 3 by lv, FINSEQ_1:def 3;
then dom vs = {1,2,3} by FINSEQ_3:1;
then d: ( 2 in dom vs & 3 in dom vs ) by ENUMSET1:def 1;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g3 by n ;
v2: vs /. (n + 1) = vs . 3 by d, n, PARTFUN1:def 6
.= g2 ;
( [60,2] in KSource & [60,3] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (cd . n) = g3 & KTarget . (cd . n) = g2 ) by cn, gg, FUNCT_1:1;
hence cd . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 2 & g2 = 0 ) ; :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 20 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [20,0] in KSource & [20,2] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (c . n) = g1 & KSource . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 2 & g2 = 1 ) ; :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 40 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [40,1] in KSource & [40,2] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (c . n) = g1 & KSource . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose ( g1 = 2 & g2 = 2 ) ; :: thesis:

end;

suppose gg: ( g1 = 2 & g2 = 3 ) ; :: thesis:

60 in KEdges by ENUMSET1:def 5;
then reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
take c ; :: thesis:
reconsider vs = <*g1,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not c is empty ; :: thesis:
l: ( len c = 1 & c . 1 = 60 ) by FINSEQ_1:40;
lv: len vs = 2 by FINSEQ_1:44;
thus vs is_vertex_seq_of c :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 60 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [60,2] in KSource & [60,3] in KTarget ) by ENUMSET1:def 5;
then ( KSource . (c . n) = g1 & KTarget . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 3 & g2 = 0 ) ; :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 30 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [30,0] in KSource & [30,3] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (c . n) = g1 & KSource . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 3 & g2 = 1 ) ; :: thesis:

reconsider g3 = 2 as Vertex of KoenigsbergBridges by ENUMSET1:def 2;
60 in KEdges by ENUMSET1:def 5;
then reconsider c = <*60*> as Path of KoenigsbergBridges by GRAPH_3:4;
40 in KEdges by ENUMSET1:def 5;
then reconsider d = <*40*> as Path of KoenigsbergBridges by GRAPH_3:4;
reconsider vs1 = <*g1,g3*> as FinSequence of the carrier of KoenigsbergBridges ;
l: ( len c = 1 & c . 1 = 60 ) by FINSEQ_1:40;
lv1: len vs1 = 2 by FINSEQ_1:44;
vs1: vs1 is_vertex_seq_of c

proof

thus len vs1 = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 60 ;
dom vs1 = Seg 2 by lv1, FINSEQ_1:def 3;
then dom vs1 = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs1 & 2 in dom vs1 ) by TARSKI:def 2;
v1: vs1 /. n = vs1 . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs1 /. (n + 1) = vs1 . 2 by d, n, PARTFUN1:def 6
.= g3 ;
( [60,2] in KSource & [60,3] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (c . n) = g1 & KSource . (c . n) = g3 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs1 /. n,vs1 /. (n + 1) by v1, v2; :: thesis:

end;

reconsider vs2 = <*g3,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
l: ( len d = 1 & d . 1 = 40 ) by FINSEQ_1:40;
lv: len vs2 = 2 by FINSEQ_1:44;
vs2: vs2 is_vertex_seq_of d

proof

thus len vs2 = (len d) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len d ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: d . n = 40 ;
dom vs2 = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs2 = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs2 & 2 in dom vs2 ) by TARSKI:def 2;
v1: vs2 /. n = vs2 . n by d, n, PARTFUN1:def 6
.= g3 by n ;
v2: vs2 /. (n + 1) = vs2 . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [40,1] in KSource & [40,2] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (d . n) = g3 & KSource . (d . n) = g2 ) by cn, gg, FUNCT_1:1;
hence d . n joins vs2 /. n,vs2 /. (n + 1) by v1, v2; :: thesis:

end;

( rng c = {60} & rng d = {40} ) by FINSEQ_1:38;
then r: rng c misses rng d by ZFMISC_1:11;
vs1 . (len vs1) = g3 by lv1
.= vs2 . 1 ;
then reconsider cd = c ^ d as Path of KoenigsbergBridges by vs1, vs2, r, GRAPH_3:6;
take cd ; :: thesis:
reconsider vs = <*g1,g3,g2*> as FinSequence of the carrier of KoenigsbergBridges ;
take vs ; :: thesis:
thus not cd is empty ; :: thesis:
cd = <*60,40*> ;
then l: ( len cd = 2 & cd . 1 = 60 & cd . 2 = 40 ) by FINSEQ_1:44;
lv: len vs = 3 by FINSEQ_1:45;
thus vs is_vertex_seq_of cd :: thesis:

proof

per cases ;

suppose n: n = 1 ; :: thesis:

then cn: cd . n = 60 by l;
dom vs = Seg 3 by lv, FINSEQ_1:def 3;
then dom vs = {1,2,3} by FINSEQ_3:1;
then d: ( 1 in dom vs & 2 in dom vs ) by ENUMSET1:def 1;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g3 ;
( [60,2] in KSource & [60,3] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (cd . n) = g1 & KSource . (cd . n) = g3 ) by cn, gg, FUNCT_1:1;
hence cd . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

suppose n: n = 2 ; :: thesis:

then cn: cd . n = 40 by l;
dom vs = Seg 3 by lv, FINSEQ_1:def 3;
then dom vs = {1,2,3} by FINSEQ_3:1;
then d: ( 2 in dom vs & 3 in dom vs ) by ENUMSET1:def 1;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g3 by n ;
v2: vs /. (n + 1) = vs . 3 by d, n, PARTFUN1:def 6
.= g2 ;
( [40,1] in KSource & [40,2] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (cd . n) = g3 & KSource . (cd . n) = g2 ) by cn, gg, FUNCT_1:1;
hence cd . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose gg: ( g1 = 3 & g2 = 2 ) ; :: thesis:

proof

thus len vs = (len c) + 1 by l, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis:
let n be Nat; :: thesis:
assume ( 1 <= n & n <= len c ) ; :: thesis:
then n: n = 1 by l, XXREAL_0:1;
then cn: c . n = 60 ;
dom vs = Seg 2 by lv, FINSEQ_1:def 3;
then dom vs = {1,2} by FINSEQ_1:2;
then d: ( 1 in dom vs & 2 in dom vs ) by TARSKI:def 2;
v1: vs /. n = vs . n by d, n, PARTFUN1:def 6
.= g1 by n ;
v2: vs /. (n + 1) = vs . 2 by d, n, PARTFUN1:def 6
.= g2 ;
( [60,2] in KSource & [60,3] in KTarget ) by ENUMSET1:def 5;
then ( KTarget . (c . n) = g1 & KSource . (c . n) = g2 ) by cn, gg, FUNCT_1:1;
hence c . n joins vs /. n,vs /. (n + 1) by v1, v2; :: thesis:

end;

thus ( vs . 1 = g1 & vs . (len vs) = g2 ) by lv; :: thesis:

end;

suppose ( g1 = 3 & g2 = 3 ) ; :: thesis:

end;

hence ( KoenigsbergBridges is finite & KoenigsbergBridges is connected ) by GRAPH_3:18; :: thesis: