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