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