consider h being FinSequence of the carrier of (TOP-REAL 2) such that

A1: h . 1 = W-min C and

A2: h is one-to-one and

A3: 8 <= len h and

A4: rng h c= C and

A5: for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C and

for i being Nat

for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),C) holds

diameter W < 1 and

for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),C) holds

diameter W < 1 and

A6: for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} and

A7: (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} and

A8: (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} and

A9: Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) and

A10: for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and

A11: for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by JORDAN7:20;

reconsider h = h as non empty FinSequence of the carrier of (TOP-REAL 2) by A3, CARD_1:27;

take h ; :: thesis: ( h /. 1 = W-min C & h is one-to-one & 8 <= len h & rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

1 in dom h by FINSEQ_5:6;

hence h /. 1 = W-min C by A1, PARTFUN1:def 6; :: thesis: ( h is one-to-one & 8 <= len h & rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus h is one-to-one by A2; :: thesis: ( 8 <= len h & rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus 8 <= len h by A3; :: thesis: ( rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus rng h c= C by A4; :: thesis: ( ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C by A5; :: thesis: ( ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} by A6; :: thesis: ( (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} by A7; :: thesis: ( (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} by A8; :: thesis: ( Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) by A9; :: thesis: ( ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) by A10; :: thesis: for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C)

thus for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by A11; :: thesis: verum

A1: h . 1 = W-min C and

A2: h is one-to-one and

A3: 8 <= len h and

A4: rng h c= C and

A5: for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C and

for i being Nat

for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),C) holds

diameter W < 1 and

for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),C) holds

diameter W < 1 and

A6: for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} and

A7: (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} and

A8: (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} and

A9: Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) and

A10: for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and

A11: for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by JORDAN7:20;

reconsider h = h as non empty FinSequence of the carrier of (TOP-REAL 2) by A3, CARD_1:27;

take h ; :: thesis: ( h /. 1 = W-min C & h is one-to-one & 8 <= len h & rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

1 in dom h by FINSEQ_5:6;

hence h /. 1 = W-min C by A1, PARTFUN1:def 6; :: thesis: ( h is one-to-one & 8 <= len h & rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus h is one-to-one by A2; :: thesis: ( 8 <= len h & rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus 8 <= len h by A3; :: thesis: ( rng h c= C & ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus rng h c= C by A4; :: thesis: ( ( for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C ) & ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus for i being Nat st 1 <= i & i < len h holds

LE h /. i,h /. (i + 1),C by A5; :: thesis: ( ( for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus for i being Nat st 1 <= i & i + 1 < len h holds

(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} by A6; :: thesis: ( (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} by A7; :: thesis: ( (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} by A8; :: thesis: ( Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) by A9; :: thesis: ( ( for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )

thus for i, j being Nat st 1 <= i & i < j & j < len h & i,j aren't_adjacent holds

Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) by A10; :: thesis: for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C)

thus for i being Nat st 1 < i & i + 1 < len h holds

Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by A11; :: thesis: verum