let z be 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:11;
then
(N-max (L~ z)) `1 <= E-bound (L~ z)
by PSCOMP_1:24;
then
(N-min (L~ z)) `1 < E-bound (L~ z)
by Th51, XXREAL_0:2;
then A4:
(N-min (L~ z)) `1 < (E-min (L~ z)) `1
by EUCLID:52;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-min (L~ z)) `2 = S-bound (L~ z) )
by EUCLID:52;
then A5:
N-min (L~ z) <> S-min (L~ z)
by TOPREAL5:16;
A6:
S-min (L~ z) in rng z
by Th41;
then A7:
(S-min (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A8:
(S-min (L~ z)) .. z <= len z
by FINSEQ_3:25;
A9:
E-min (L~ z) in rng z
by Th45;
then A10:
(E-min (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A11: z /. ((E-min (L~ z)) .. z) =
z . ((E-min (L~ z)) .. z)
by PARTFUN1:def 6
.=
E-min (L~ z)
by A9, FINSEQ_4:19
;
A12:
W-min (L~ z) in rng z
by Th43;
then A13:
(W-min (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A14: z /. ((W-min (L~ z)) .. z) =
z . ((W-min (L~ z)) .. z)
by PARTFUN1:def 6
.=
W-min (L~ z)
by A12, FINSEQ_4:19
;
A15:
1 <= (W-min (L~ z)) .. z
by A13, FINSEQ_3:25;
( (W-min (L~ z)) `1 = W-bound (L~ z) & (E-min (L~ z)) `1 = E-bound (L~ z) )
by EUCLID:52;
then
z /. ((E-min (L~ z)) .. z) <> z /. ((W-min (L~ z)) .. z)
by A14, A11, TOPREAL5:17;
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 6
.=
S-min (L~ z)
by A6, FINSEQ_4:19
;
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, Th38;
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, Th9;
then A20:
(h /. (len h)) `2 = N-bound (L~ z)
by A3, EUCLID:52;
(E-min (L~ z)) .. z <= len z
by A10, FINSEQ_3:25;
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, Th38;
M /. (len M) =
z /. ((E-min (L~ z)) .. z)
by A10, A13, Th9
.=
E-min (L~ z)
by A9, FINSEQ_5:38
;
then A21:
(M /. (len M)) `1 = E-bound (L~ z)
by EUCLID:52;
z /. ((S-min (L~ z)) .. z) =
z . ((S-min (L~ z)) .. z)
by A7, PARTFUN1:def 6
.=
S-min (L~ z)
by A6, FINSEQ_4:19
;
then
h /. 1 = S-min (L~ z)
by A19, A7, Th8;
then A22:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:52;
h is_in_the_area_of z
by A19, A7, Th21, Th22;
then A23:
h is_a_v.c._for z
by A22, A20;
( W-max (L~ z) in L~ z & (N-min (L~ z)) `2 = N-bound (L~ z) )
by EUCLID:52, SPRECT_1:13;
then
(W-max (L~ z)) `2 <= (N-min (L~ z)) `2
by PSCOMP_1:24;
then
N-min (L~ z) <> W-min (L~ z)
by Th57;
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, Th47;
M /. 1 = W-min (L~ z)
by A10, A13, A14, Th8;
then A25:
(M /. 1) `1 = W-bound (L~ z)
by EUCLID:52;
M is_in_the_area_of z
by A10, A13, Th21, Th22;
then A26:
M is_a_h.c._for z
by A25, A21;
( len h >= 2 & len M >= 2 )
by TOPREAL1:def 8;
hence
contradiction
by A23, A26, A24, Th29; verum