let z be non constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = N-min (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set i1 = (E-min (L~ z)) .. z;
set i2 = (W-min (L~ z)) .. z;
set j = (S-min (L~ z)) .. z;
assume that
A1:
z /. 1 = N-min (L~ z)
and
A2:
( S-min (L~ z) <> W-min (L~ z) & (S-min (L~ z)) .. z >= (W-min (L~ z)) .. z )
; contradiction
A3:
z /. (len z) = N-min (L~ z)
by A1, FINSEQ_6:def 1;
N-max (L~ z) in L~ z
by SPRECT_1:13;
then
(N-max (L~ z)) `1 <= E-bound (L~ z)
by PSCOMP_1:71;
then
(N-min (L~ z)) `1 < E-bound (L~ z)
by Th55, XXREAL_0:2;
then A4:
(N-min (L~ z)) `1 < (E-min (L~ z)) `1
by EUCLID:56;
A5:
E-min (L~ z) in rng z
by Th49;
then A6:
(E-min (L~ z)) .. z in dom z
by FINSEQ_4:30;
then A7:
1 <= (E-min (L~ z)) .. z
by FINSEQ_3:27;
then A8:
(S-min (L~ z)) .. z > 1
by A1, Lm9, XXREAL_0:2;
z /. ((E-min (L~ z)) .. z) =
z . ((E-min (L~ z)) .. z)
by A6, PARTFUN1:def 8
.=
E-min (L~ z)
by A5, FINSEQ_4:29
;
then A9:
(E-min (L~ z)) .. z > 1
by A1, A7, A4, XXREAL_0:1;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-min (L~ z)) `2 = S-bound (L~ z) )
by EUCLID:56;
then A10:
N-min (L~ z) <> S-min (L~ z)
by TOPREAL5:22;
A11:
S-min (L~ z) in rng z
by Th45;
then A12:
(S-min (L~ z)) .. z in dom z
by FINSEQ_4:30;
then A13:
(S-min (L~ z)) .. z <= len z
by FINSEQ_3:27;
z /. ((S-min (L~ z)) .. z) =
z . ((S-min (L~ z)) .. z)
by A12, PARTFUN1:def 8
.=
S-min (L~ z)
by A11, FINSEQ_4:29
;
then
(S-min (L~ z)) .. z < len z
by A3, A13, A10, XXREAL_0:1;
then reconsider h = mid z,((S-min (L~ z)) .. z),(len z) as S-Sequence_in_R2 by A8, Th42;
A14:
len z in dom z
by FINSEQ_5:6;
then
h /. (len h) = z /. (len z)
by A12, Th13;
then A15:
(h /. (len h)) `2 = N-bound (L~ z)
by A3, EUCLID:56;
A16: z /. ((S-min (L~ z)) .. z) =
z . ((S-min (L~ z)) .. z)
by A12, PARTFUN1:def 8
.=
S-min (L~ z)
by A11, FINSEQ_4:29
;
then
h /. 1 = S-min (L~ z)
by A12, A14, Th12;
then A17:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:56;
h is_in_the_area_of z
by A12, A14, Th25, Th26;
then A18:
h is_a_v.c._for z
by A17, A15, Def3;
A19:
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z
by A1, Lm11;
A20:
W-min (L~ z) in rng z
by Th47;
then A21:
(W-min (L~ z)) .. z in dom z
by FINSEQ_4:30;
then
(W-min (L~ z)) .. z <= len z
by FINSEQ_3:27;
then reconsider M = mid z,((W-min (L~ z)) .. z),((E-min (L~ z)) .. z) as S-Sequence_in_R2 by A19, A9, Th41;
M /. (len M) =
z /. ((E-min (L~ z)) .. z)
by A6, A21, Th13
.=
E-min (L~ z)
by A5, FINSEQ_5:41
;
then A22:
(M /. (len M)) `1 = E-bound (L~ z)
by EUCLID:56;
A23: z /. ((W-min (L~ z)) .. z) =
z . ((W-min (L~ z)) .. z)
by A21, PARTFUN1:def 8
.=
W-min (L~ z)
by A20, FINSEQ_4:29
;
then
M /. 1 = W-min (L~ z)
by A6, A21, Th12;
then A24:
(M /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
M is_in_the_area_of z
by A6, A21, Th25, Th26;
then A25:
M is_a_h.c._for z
by A24, A22, Def2;
A26:
( len h >= 2 & len M >= 2 )
by TOPREAL1:def 10;
(S-min (L~ z)) .. z > (W-min (L~ z)) .. z
by A2, A23, A16, XXREAL_0:1;
then
L~ M misses L~ h
by A19, A9, A13, Th54;
hence
contradiction
by A18, A26, A25, Th33; verum