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