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
; ( 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; ( 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; ( 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; ( 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; ( ( 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; ( ( 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; ( (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; ( (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; ( 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; ( ( 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; 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; verum