let G be _finite chordal _Graph; :: thesis: for L being PartFunc of (the_Vertices_of G),NAT st L is with_property_T & dom L = the_Vertices_of G holds
for V being VertexScheme of G st V " = L holds
V is perfect
let L be PartFunc of (the_Vertices_of G),NAT; :: thesis: ( L is with_property_T & dom L = the_Vertices_of G implies for V being VertexScheme of G st V " = L holds
V is perfect )
assume that
A1: L is with_property_T and
A2: dom L = the_Vertices_of G ; :: thesis: for V being VertexScheme of G st V " = L holds
V is perfect
defpred S₁[ Path of G] means ( len $1 >= 5 & $1 is open & $1 is chordless & L . ($1 .first()) > L . ($1 .last()) & L . ($1 .last()) > L . ($1 . 3) & ex i being odd Element of NAT st
( 1 < i & i < len $1 & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len $1 holds
L . ($1 . j) < L . ($1 . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . ($1 . j) > L . ($1 . k) ) ) );
let V be VertexScheme of G; :: thesis: ( V " = L implies V is perfect )
assume A3: V " = L ; :: thesis: V is perfect
A4: V is one-to-one by CHORD:def 12;
len V = card (the_Vertices_of G) by CHORD:104;
then dom V = Seg (G .order()) by FINSEQ_1:def 3;
then A5: rng L = Seg (G .order()) by A3, A4, FUNCT_1:33;

A6: now :: thesis: for R being Path of G holds not S₁[R]

defpred S₂[ Nat] means ex P being Path of G st
( S₁[P] & L . (P .last()) = $1 );
A7: for k being Nat st S₂[k] holds
k <= G .order()

proof

let k be Nat; :: thesis: ( S₂[k] implies k <= G .order() )
assume S₂[k] ; :: thesis: k <= G .order()
then consider P being Path of G such that
S₁[P] and
A8: L . (P .last()) = k ;
L . (P .last()) in Seg (G .order()) by A2, A5, FUNCT_1:def 3;
hence k <= G .order() by A8, FINSEQ_1:1; :: thesis: verum

end;

let R be Path of G; :: thesis: not S₁[R]
assume S₁[R] ; :: thesis: contradiction
then A9: ex k being Nat st S₂[k] ;
consider k being Nat such that
A10: S₂[k] and
A11: for n being Nat st S₂[n] holds
n <= k from NAT_1:sch 6(A7, A9);
consider P being Path of G such that
A12: S₁[P] and
A13: L . (P .last()) = k by A10;
3 <= len P by A12, XXREAL_0:2;
then P . 3 = P .vertexAt ((2 * 1) + 1) by GLIB_001:def 8;
then reconsider a = P . 3 as Vertex of G ;
A14: 3 < len P by A12, XXREAL_0:2;
reconsider b = P .last() as Vertex of G ;
reconsider c = P .first() as Vertex of G ;

A15: now :: thesis: for e being object holds not e Joins c,b,G

(2 * 0) + 1 < len P by A12, XXREAL_0:2;
then A16: ( ex e being object st e Joins P . 1,P . (len P),G iff 1 + 2 = len P ) by A12, CHORD:92;
let e be object ; :: thesis: not e Joins c,b,G
assume e Joins c,b,G ; :: thesis: contradiction
hence contradiction by A12, A16; :: thesis: verum

end;

then A17: not b,c are_adjacent by CHORD:def 3;
(2 * 0) + 1 < (2 * 1) + 1 ;
then ex ez being object st ez Joins P . 1,P . 3,G by A12, A14, CHORD:92;
then c,a are_adjacent by CHORD:def 3;
then consider d being Vertex of G such that
d in dom L and
A18: L . b < L . d and
A19: b,d are_adjacent and
A20: not a,d are_adjacent by A1, A2, A12, A17;
A21: L . d <> L . c by A2, A3, A4, A17, A19, FUNCT_1:def 4;
consider i being odd Element of NAT such that
A22: 1 < i and
i < len P and
A23: for j, k being odd Element of NAT st i <= j & j < k & k <= len P holds
L . (P . j) < L . (P . k) and
A24: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (P . j) > L . (P . k) by A12;
A25: L . a < L . d by A12, A18, XXREAL_0:2;

A26: now :: thesis: not d in P .vertices()

assume d in P .vertices() ; :: thesis: contradiction
then consider dn being odd Element of NAT such that
A27: dn <= len P and
A28: P . dn = d by GLIB_001:87;
A29: 1 <= dn by CHORD:2;
dn <> 1 by A15, A19, A28, CHORD:def 3;
then (2 * 0) + 1 < dn by A29, XXREAL_0:1;
then 1 + 2 <= dn by CHORD:4;
then A30: (2 * 1) + 1 < dn by A12, A18, A28, XXREAL_0:1;
A31: dn < len P by A18, A27, A28, XXREAL_0:1;

per cases ( i <= dn or dn < i ) ;

suppose i <= dn ; :: thesis: contradiction

hence contradiction by A23, A18, A28, A31; :: thesis: verum

end;

suppose dn < i ; :: thesis: contradiction

hence contradiction by A24, A25, A28, A30; :: thesis: verum

end;

end;

end;

defpred S₃[ Nat] means ( $1 is odd & 3 < $1 & $1 <= len P & ex e being object st e Joins P . $1,d,G );
ex el being object st el Joins P .last() ,d,G by A19, CHORD:def 3;
then A32: ex k being Nat st S₃[k] by A14;
ex j being Nat st
( S₃[j] & ( for n being Nat st S₃[n] holds
j <= n ) ) from NAT_1:sch 5(A32);
then consider j being Nat such that
A33: j is odd and
A34: 3 < j and
A35: j <= len P and
A36: ex e being object st e Joins P . j,d,G and
A37: for i being Nat st S₃[i] holds
j <= i ;
reconsider j = j as odd Element of NAT by A33, ORDINAL1:def 12;
reconsider C = P .cut (1,j) as Path of G ;
consider e being object such that
A38: e Joins P . j,d,G by A36;
(2 * 0) + 1 < j by A34, XXREAL_0:2;
then A39: ( C is open & C is chordless ) by A12, A35, CHORD:93;
A40: (2 * 0) + 1 <= j by CHORD:2;
then A41: (len C) + 1 = j + 1 by A35, GLIB_001:36;

A42: now :: thesis: for n being odd Element of NAT st n <= j holds
C . n = P . n

let n be odd Element of NAT ; :: thesis: ( n <= j implies C . n = P . n )
assume A43: n <= j ; :: thesis: C . n = P . n
1 <= n by CHORD:2;
then n in dom C by A41, A43, FINSEQ_3:25;
then C . n = P . ((1 + n) - 1) by A35, A40, GLIB_001:47;
hence C . n = P . n ; :: thesis: verum

end;

(2 * 1) + 1 < j by A34;
then A44: C . 3 = a by A42;

A45: now :: thesis: for f being object holds not f Joins C . ((len C) - 2),d,G

len C > (2 * 1) + 1 by A34, A41;
then A46: len C >= 3 + 2 by CHORD:4;
let f be object ; :: thesis: not f Joins C . ((len C) - 2),d,G
assume A47: f Joins C . ((len C) - 2),d,G ; :: thesis: contradiction
len C <> 5 by A20, A44, A47, CHORD:def 3;
then len C > 5 by A46, XXREAL_0:1;
then A48: (3 + 2) - 2 < (len C) - 2 by XREAL_1:9;
then 0 < (len C) - (2 * 1) ;
then reconsider cc = (len C) - 2 as odd Element of NAT by INT_1:3;
A49: cc < len C by XREAL_1:44;
then A50: cc < len P by A35, A41, XXREAL_0:2;
f Joins P . cc,d,G by A41, A42, A47, A49;
hence contradiction by A37, A41, A48, A49, A50; :: thesis: verum

end;

A51: e Joins C .last() ,d,G by A35, A38, A40, GLIB_001:37;
C .vertices() c= P .vertices() by A35, A40, GLIB_001:94;
then A52: not d in C .vertices() by A26;
then reconsider D = C .addEdge e as Path of G by A51, A39, A45, CHORD:97;
reconsider R = D .reverse() as Path of G ;
A53: C .last() = P . j by A35, A40, GLIB_001:37;
then A54: len D = (len C) + 2 by A38, GLIB_001:64;

A55: now :: thesis: L . (P . j) < L . c

per cases ( i < j or i >= j ) ;

suppose A56: i < j ; :: thesis: L . (P . j) < L . c

now :: thesis: L . (P . j) <= L . b

per cases ( j = len P or j < len P ) by A35, XXREAL_0:1;

suppose j = len P ; :: thesis: L . (P . j) <= L . b

hence L . (P . j) <= L . b ; :: thesis: verum

end;

suppose j < len P ; :: thesis: L . (P . j) <= L . b

hence L . (P . j) <= L . b by A23, A56; :: thesis: verum

end;

end;

end;

hence L . (P . j) < L . c by A12, XXREAL_0:2; :: thesis: verum

end;

suppose A57: i >= j ; :: thesis: L . (P . j) < L . c

1 < (2 * 1) + 1 ;
then L . (P . j) < L . (P . 3) by A24, A34, A57;
then L . (P . j) < L . b by A12, XXREAL_0:2;
hence L . (P . j) < L . c by A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

C .first() = P .first() by A35, A40, GLIB_001:37;
then A58: D .first() = c by A38, A53, GLIB_001:63;
then A59: R .last() = c by GLIB_001:22;
3 in dom C by A34, A41, FINSEQ_3:25;
then A60: D . 3 = a by A38, A53, A44, GLIB_001:65;
A61: D is chordless by A52, A51, A39, A45, CHORD:97;
A62: D .last() = d by A38, A53, GLIB_001:63;
then A63: R .first() = d by GLIB_001:22;
A64: for n being odd Element of NAT st n <= len R holds
( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT )

proof

let n be odd Element of NAT ; :: thesis: ( n <= len R implies ( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT ) )
assume A65: n <= len R ; :: thesis: ( R . n = D . (((len D) - n) + 1) & ((len D) - n) + 1 is Element of NAT )
1 <= n by CHORD:2;
then A66: n in dom R by A65, FINSEQ_3:25;
hence R . n = D . (((len D) - n) + 1) by GLIB_001:25; :: thesis: ((len D) - n) + 1 is Element of NAT
((len D) - n) + 1 in dom D by A66, GLIB_001:25;
hence ((len D) - n) + 1 is Element of NAT ; :: thesis: verum

end;

A67: now :: thesis: for n being odd Nat st n <= j holds
C . n = D . n

let n be odd Nat; :: thesis: ( n <= j implies C . n = D . n )
assume A68: n <= j ; :: thesis: C . n = D . n
1 <= n by CHORD:2;
then n in dom C by A41, A68, FINSEQ_3:25;
hence C . n = D . n by A51, GLIB_001:65; :: thesis: verum

end;

A69: ex i being odd Element of NAT st
( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) ) )

proof

per cases ( j <= i or i < j ) ;

suppose A70: j <= i ; :: thesis: ex i being odd Element of NAT st
( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) ) )

A71: now :: thesis: for e, f being odd Element of NAT st j <= e & e < f & f <= len D holds
L . (D . e) < L . (D . f)

1 < (2 * 1) + 1 ;
then A72: L . (P . 3) > L . (P . j) by A24, A34, A70;
let e, f be odd Element of NAT ; :: thesis: ( j <= e & e < f & f <= len D implies L . (D . e) < L . (D . f) )
assume that
A73: j <= e and
A74: e < f and
A75: f <= len D ; :: thesis: L . (D . e) < L . (D . f)
e < j + (2 * 1) by A41, A54, A74, A75, XXREAL_0:2;
then e <= (j + 2) - 2 by CHORD:3;
then A76: e = j by A73, XXREAL_0:1;
then D . e = C . j by A67;
then A77: D . e = P . j by A42;
(len C) + 2 <= f by A41, A74, A76, CHORD:4;
then D . f = d by A54, A62, A75, XXREAL_0:1;
hence L . (D . e) < L . (D . f) by A25, A77, A72, XXREAL_0:2; :: thesis: verum

end;

take j ; :: thesis: ( 1 < j & j < len D & ( for j, k being odd Element of NAT st j <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= j holds
L . (D . j) > L . (D . k) ) )

now :: thesis: for e, f being odd Element of NAT st 1 <= e & e < f & f <= j holds
L . (D . e) > L . (D . f)

let e, f be odd Element of NAT ; :: thesis: ( 1 <= e & e < f & f <= j implies L . (D . e) > L . (D . f) )
assume that
A78: 1 <= e and
A79: e < f and
A80: f <= j ; :: thesis: L . (D . e) > L . (D . f)
D . e = C . e by A67, A79, A80, XXREAL_0:2;
then A81: D . e = P . e by A42, A79, A80, XXREAL_0:2;
D . f = C . f by A67, A80;
then A82: D . f = P . f by A42, A80;
f <= i by A70, A80, XXREAL_0:2;
hence L . (D . e) > L . (D . f) by A24, A78, A79, A81, A82; :: thesis: verum

end;

hence ( 1 < j & j < len D & ( for j, k being odd Element of NAT st j <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= j holds
L . (D . j) > L . (D . k) ) ) by A34, A41, A54, A71, XREAL_1:29, XXREAL_0:2; :: thesis: verum

end;

suppose A83: i < j ; :: thesis: ex i being odd Element of NAT st
( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) ) )

take i ; :: thesis: ( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) ) )

A84: now :: thesis: for e, f being odd Element of NAT st i <= e & e < f & f <= len D holds
L . (D . e) < L . (D . f)

let e, f be odd Element of NAT ; :: thesis: ( i <= e & e < f & f <= len D implies L . (D . b₁) < L . (D . b₂) )
assume that
A85: i <= e and
A86: e < f and
A87: f <= len D ; :: thesis: L . (D . b₁) < L . (D . b₂)
e < j + (2 * 1) by A41, A54, A86, A87, XXREAL_0:2;
then A88: e <= (j + 2) - 2 by CHORD:3;
then A89: e <= len P by A35, XXREAL_0:2;
A90: D . e = C . e by A67, A88;
then A91: D . e = P . e by A42, A88;

per cases ( f = len D or f < len D ) by A87, XXREAL_0:1;

suppose A92: f = len D ; :: thesis: L . (D . b₁) < L . (D . b₂)

now :: thesis: L . (D . e) <= L . b

per cases ( e = len P or e < len P ) by A89, XXREAL_0:1;

suppose e = len P ; :: thesis: L . (D . e) <= L . b

hence L . (D . e) <= L . b by A42, A88, A90; :: thesis: verum

end;

suppose e < len P ; :: thesis: L . (D . e) <= L . b

hence L . (D . e) <= L . b by A23, A85, A91; :: thesis: verum

end;

end;

end;

hence L . (D . e) < L . (D . f) by A18, A62, A92, XXREAL_0:2; :: thesis: verum

end;

suppose f < len D ; :: thesis: L . (D . b₁) < L . (D . b₂)

then A93: f <= (j + 2) - 2 by A41, A54, CHORD:3;
then D . f = C . f by A67;
then A94: D . f = P . f by A42, A93;
f <= len P by A35, A93, XXREAL_0:2;
hence L . (D . e) < L . (D . f) by A23, A85, A86, A91, A94; :: thesis: verum

end;

end;

end;

A95: now :: thesis: for e, f being odd Element of NAT st 1 <= e & e < f & f <= i holds
L . (D . e) > L . (D . f)

let e, f be odd Element of NAT ; :: thesis: ( 1 <= e & e < f & f <= i implies L . (D . e) > L . (D . f) )
assume that
A96: 1 <= e and
A97: e < f and
A98: f <= i ; :: thesis: L . (D . e) > L . (D . f)
D . f = C . f by A67, A83, A98, XXREAL_0:2;
then A99: D . f = P . f by A42, A83, A98, XXREAL_0:2;
A100: e <= i by A97, A98, XXREAL_0:2;
then D . e = C . e by A67, A83, XXREAL_0:2;
then D . e = P . e by A42, A83, A100, XXREAL_0:2;
hence L . (D . e) > L . (D . f) by A24, A96, A97, A98, A99; :: thesis: verum

end;

len D > j by A41, A54, XREAL_1:29;
hence ( 1 < i & i < len D & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) ) ) by A22, A83, A84, A95, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A101: ex i being odd Element of NAT st
( 1 < i & i < len R & ( for j, k being odd Element of NAT st i <= j & j < k & k <= len R holds
L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (R . j) > L . (R . k) ) )

proof

consider i being odd Element of NAT such that
A102: 1 < i and
A103: i < len D and
A104: for j, k being odd Element of NAT st i <= j & j < k & k <= len D holds
L . (D . j) < L . (D . k) and
A105: for j, k being odd Element of NAT st 1 <= j & j < k & k <= i holds
L . (D . j) > L . (D . k) by A69;
set ir = ((len D) - i) + 1;
(len D) - 1 > (len D) - i by A102, XREAL_1:15;
then A106: ((len D) - 1) + 1 > ((len D) - i) + 1 by XREAL_1:8;
then A107: ((len D) - i) + 1 < len R by GLIB_001:21;
A108: (len D) - (len D) < (len D) - i by A103, XREAL_1:15;
then reconsider ir = ((len D) - i) + 1 as odd Element of NAT by INT_1:3;

A109: now :: thesis: for ja, k being odd Element of NAT st 1 <= ja & ja < k & k <= ir holds
L . (R . ja) > L . (R . k)

let ja, k be odd Element of NAT ; :: thesis: ( 1 <= ja & ja < k & k <= ir implies L . (R . ja) > L . (R . k) )
assume that
A110: 1 <= ja and
A111: ja < k and
A112: k <= ir ; :: thesis: L . (R . ja) > L . (R . k)
set jr = ((len D) - ja) + 1;
A113: k <= len R by A107, A112, XXREAL_0:2;
then A114: ja <= len R by A111, XXREAL_0:2;
then A115: R . ja = D . (((len D) - ja) + 1) by A64;
i + k <= (((len D) - i) + 1) + i by A112, XREAL_1:7;
then A116: (i + k) - k <= ((len D) + 1) - k by XREAL_1:9;
set kr = ((len D) - k) + 1;
A117: ((len D) - k) + 1 < ((len D) - ja) + 1 by A111, Lm3;
reconsider jr = ((len D) - ja) + 1 as odd Element of NAT by A64, A114;
reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A64, A113;
(len D) - ja <= (len D) - 1 by A110, XREAL_1:10;
then jr <= ((len D) - 1) + 1 by XREAL_1:7;
then L . (D . kr) < L . (D . jr) by A104, A116, A117;
hence L . (R . ja) > L . (R . k) by A64, A113, A115; :: thesis: verum

end;

take ir ; :: thesis: ( 1 < ir & ir < len R & ( for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds
L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= ir holds
L . (R . j) > L . (R . k) ) )

A118: now :: thesis: for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds
L . (R . j) < L . (R . k)

let j, k be odd Element of NAT ; :: thesis: ( ir <= j & j < k & k <= len R implies L . (R . j) < L . (R . k) )
assume that
A119: ir <= j and
A120: j < k and
A121: k <= len R ; :: thesis: L . (R . j) < L . (R . k)
set kr = ((len D) - k) + 1;
A122: R . k = D . (((len D) - k) + 1) by A64, A121;
set jr = ((len D) - j) + 1;
A123: j <= len R by A120, A121, XXREAL_0:2;
then A124: R . j = D . (((len D) - j) + 1) by A64;
reconsider kr = ((len D) - k) + 1 as odd Element of NAT by A64, A121;
i + j >= (((len D) - i) + 1) + i by A119, XREAL_1:7;
then A125: (i + j) - j >= ((len D) + 1) - j by XREAL_1:9;
reconsider jr = ((len D) - j) + 1 as odd Element of NAT by A64, A123;
kr < jr by A120, Lm3;
hence L . (R . j) < L . (R . k) by A105, A124, A122, A125, CHORD:2; :: thesis: verum

end;

0 + 1 < ((len D) - i) + 1 by A108, XREAL_1:8;
hence ( 1 < ir & ir < len R & ( for j, k being odd Element of NAT st ir <= j & j < k & k <= len R holds
L . (R . j) < L . (R . k) ) & ( for j, k being odd Element of NAT st 1 <= j & j < k & k <= ir holds
L . (R . j) > L . (R . k) ) ) by A106, A118, A109, GLIB_001:21; :: thesis: verum

end;

A126: len D >= 3 + 2 by A34, A41, A54, XREAL_1:7;
then A127: len R >= 3 + 2 by GLIB_001:21;
then 3 <= len R by XXREAL_0:2;
then 3 in dom R by FINSEQ_3:25;
then R . 3 = D . (((len D) - 3) + 1) by GLIB_001:25;
then R . 3 = C . j by A41, A54, A67;
then A128: L . (R .last()) > L . (R . 3) by A42, A59, A55;
d <> c by A15, A19, CHORD:def 3;
then A129: R is open by A63, A59;
D is open by A52, A51, A39, A45, CHORD:97;
then L . c <= L . d by A11, A13, A18, A25, A61, A126, A58, A62, A60, A69;
then A130: L . c < L . d by A21, XXREAL_0:1;
R is chordless by A61, CHORD:91;
hence contradiction by A11, A12, A13, A130, A63, A59, A129, A127, A128, A101; :: thesis: verum

end;

A131: L " = V by A3, A4, FUNCT_1:43;

now :: thesis: for a, b, c being Vertex of G st b <> c & a,b are_adjacent & a,c are_adjacent holds
for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds
b,c are_adjacent

let a, b, c be Vertex of G; :: thesis: ( b <> c & a,b are_adjacent & a,c are_adjacent implies for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds
b,c are_adjacent )
assume that
A132: b <> c and
A133: a,b are_adjacent and
A134: a,c are_adjacent ; :: thesis: for va, vb, vc being Nat st va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc holds
b,c are_adjacent
let va, vb, vc be Nat; :: thesis: ( va in dom V & vb in dom V & vc in dom V & V . va = a & V . vb = b & V . vc = c & va < vb & va < vc implies b,c are_adjacent )
assume that
A135: va in dom V and
A136: vb in dom V and
A137: vc in dom V and
A138: V . va = a and
A139: V . vb = b and
A140: V . vc = c and
A141: va < vb and
A142: va < vc ; :: thesis: b,c are_adjacent
A143: L . a = va by A3, A4, A135, A138, FUNCT_1:34;
A144: c = V . (L . c) by A2, A3, A4, A131, FUNCT_1:34;
A145: b = V . (L . b) by A2, A3, A4, A131, FUNCT_1:34;
assume A146: not b,c are_adjacent ; :: thesis: contradiction
A147: L . b = vb by A3, A4, A136, A139, FUNCT_1:34;
A148: L . c = vc by A3, A4, A137, A140, FUNCT_1:34;

per cases ( L . b < L . c or L . c < L . b ) by A132, A145, A144, XXREAL_0:1;

suppose A149: L . b < L . c ; :: thesis: contradiction

A150: (2 * 1) + 1 is odd ;
consider P being Path of G, e1, e2 being object such that
A151: P is open and
A152: len P = 5 and
P .length() = 2 and
e1 Joins c,a,G and
e2 Joins a,b,G and
P .edges() = {e1,e2} and
P .vertices() = {c,a,b} and
A153: P . 1 = c and
A154: P . 3 = a and
A155: P . 5 = b by A132, A133, A134, A141, A142, A143, A147, A148, CHORD:47;
A156: P .first() = c by A153;

A157: now :: thesis: for j, k being odd Element of NAT st 1 <= j & j < k & k <= 3 holds
L . (P . j) > L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 1 <= j & j < k & k <= 3 implies L . (P . j) > L . (P . k) )
assume that
1 <= j and
A158: j < k and
A159: k <= 3 ; :: thesis: L . (P . j) > L . (P . k)
j < 3 by A158, A159, XXREAL_0:2;
then j = 1 by CHORD:7, XXREAL_0:2;
hence L . (P . j) > L . (P . k) by A142, A143, A148, A153, A154, A158, A159, CHORD:7, XXREAL_0:2; :: thesis: verum

end;

A160: now :: thesis: for j, k being odd Element of NAT st 3 <= j & j < k & k <= len P holds
L . (P . j) < L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 3 <= j & j < k & k <= len P implies L . (P . j) < L . (P . k) )
assume that
A161: 3 <= j and
A162: j < k and
A163: k <= len P ; :: thesis: L . (P . j) < L . (P . k)
j < 5 by A152, A162, A163, XXREAL_0:2;
then ( j = 1 or j = 3 or j = 5 ) by CHORD:8, XXREAL_0:2;
hence L . (P . j) < L . (P . k) by A141, A142, A143, A147, A148, A152, A153, A154, A155, A161, A162, A163, CHORD:8, XXREAL_0:2; :: thesis: verum

end;

P .last() = b by A152, A155;
then S₁[P] by A146, A149, A151, A152, A156, A160, A157, A150, CHORD:90;
hence contradiction by A6; :: thesis: verum

end;

suppose A164: L . c < L . b ; :: thesis: contradiction

A165: (2 * 1) + 1 is odd ;
consider P being Path of G, e1, e2 being object such that
A166: P is open and
A167: len P = 5 and
P .length() = 2 and
e1 Joins b,a,G and
e2 Joins a,c,G and
P .edges() = {e1,e2} and
P .vertices() = {b,a,c} and
A168: P . 1 = b and
A169: P . 3 = a and
A170: P . 5 = c by A132, A133, A134, A141, A142, A143, A147, A148, CHORD:47;
A171: P .first() = b by A168;

A172: now :: thesis: for j, k being odd Element of NAT st 1 <= j & j < k & k <= 3 holds
L . (P . j) > L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 1 <= j & j < k & k <= 3 implies L . (P . j) > L . (P . k) )
assume that
1 <= j and
A173: j < k and
A174: k <= 3 ; :: thesis: L . (P . j) > L . (P . k)
j < 3 by A173, A174, XXREAL_0:2;
then j = 1 by CHORD:7, XXREAL_0:2;
hence L . (P . j) > L . (P . k) by A141, A143, A147, A168, A169, A173, A174, CHORD:7, XXREAL_0:2; :: thesis: verum

end;

A175: now :: thesis: for j, k being odd Element of NAT st 3 <= j & j < k & k <= len P holds
L . (P . j) < L . (P . k)

let j, k be odd Element of NAT ; :: thesis: ( 3 <= j & j < k & k <= len P implies L . (P . j) < L . (P . k) )
assume that
A176: 3 <= j and
A177: j < k and
A178: k <= len P ; :: thesis: L . (P . j) < L . (P . k)
j < 5 by A167, A177, A178, XXREAL_0:2;
then ( j = 1 or j = 3 or j = 5 ) by CHORD:8, XXREAL_0:2;
hence L . (P . j) < L . (P . k) by A141, A142, A143, A147, A148, A167, A168, A169, A170, A176, A177, A178, CHORD:8, XXREAL_0:2; :: thesis: verum

end;

P .last() = c by A167, A170;
then S₁[P] by A146, A164, A166, A167, A171, A175, A172, A165, CHORD:90;
hence contradiction by A6; :: thesis: verum

end;

end;

end;

hence V is perfect by CHORD:109; :: thesis: verum