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 Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C
and
for i being Element of 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 Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C
and
A11:
for i being Element of 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:21;
reconsider h = h as non empty FinSequence of the carrier of (TOP-REAL 2) by A3, CARD_1:47;
take
h
; ( h /. 1 = W-min C & h is one-to-one & 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 8; ( h is one-to-one & 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C
by A5; ( ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C ) & ( for i being Element of 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 Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),C misses Segment (h /. j),(h /. (j + 1)),C
by A10; for i being Element of 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 Element of 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