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 (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set i1 = (W-min (L~ z)) .. z;
set i2 = (W-max (L~ z)) .. z;
set j = (E-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:
(W-min (L~ z)) .. z >= (W-max (L~ z)) .. z
; contradiction
A4:
(W-max (L~ z)) .. z > (E-min (L~ z)) .. z
by A1, A2, Lm10;
A5:
E-min (L~ z) in rng z
by Th45;
then A6:
(E-min (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A7: z /. ((E-min (L~ z)) .. z) =
z . ((E-min (L~ z)) .. z)
by PARTFUN1:def 6
.=
E-min (L~ z)
by A5, FINSEQ_4:19
;
then A8:
(z /. ((E-min (L~ z)) .. z)) `1 = E-bound (L~ z)
by EUCLID:52;
A9:
(E-min (L~ z)) .. z <= len z
by A6, FINSEQ_3:25;
A10:
z /. (len z) = N-min (L~ z)
by A1, FINSEQ_6:def 1;
A11:
W-max (L~ z) in rng z
by Th44;
then A12:
(W-max (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A13:
1 <= (W-max (L~ z)) .. z
by FINSEQ_3:25;
A14:
W-min (L~ z) in rng z
by Th43;
then A15:
(W-min (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A16: z /. ((W-min (L~ z)) .. z) =
z . ((W-min (L~ z)) .. z)
by PARTFUN1:def 6
.=
W-min (L~ z)
by A14, FINSEQ_4:19
;
A17:
(W-min (L~ z)) .. z <= len z
by A15, FINSEQ_3:25;
( 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
( z /. 1 = z /. (len z) & N-min (L~ z) <> W-min (L~ z) )
by Th57, FINSEQ_6:def 1;
then A18:
(W-min (L~ z)) .. z < len z
by A1, A17, A16, XXREAL_0:1;
then
((W-min (L~ z)) .. z) + 1 <= len z
by NAT_1:13;
then
(len z) - ((W-min (L~ z)) .. z) >= 1
by XREAL_1:19;
then
(len z) -' ((W-min (L~ z)) .. z) >= 1
by NAT_D:39;
then A19:
((len z) -' ((W-min (L~ z)) .. z)) + 1 >= 1 + 1
by XREAL_1:6;
A20:
1 <= (E-min (L~ z)) .. z
by A6, FINSEQ_3:25;
then
(W-min (L~ z)) .. z > 1
by A1, Lm11, XXREAL_0:2;
then reconsider M = mid (z,((W-min (L~ z)) .. z),(len z)) as S-Sequence_in_R2 by A18, Th38;
A21:
len z in dom z
by FINSEQ_5:6;
then A22:
M /. 1 = z /. ((W-min (L~ z)) .. z)
by A15, Th8;
1 <= (W-min (L~ z)) .. z
by A15, FINSEQ_3:25;
then A23:
len M = ((len z) -' ((W-min (L~ z)) .. z)) + 1
by A17, FINSEQ_6:186;
A24:
M is_in_the_area_of z
by A15, A21, Th21, Th22;
A25:
M /. (len M) = z /. (len z)
by A15, A21, Th9;
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
(N-min (L~ z)) `1 < (E-min (L~ z)) `1
by EUCLID:52;
then A26:
1 < (E-min (L~ z)) .. z
by A1, A20, A7, XXREAL_0:1;
A27:
(W-max (L~ z)) .. z <= len z
by A12, FINSEQ_3:25;
then reconsider h = mid (z,((W-max (L~ z)) .. z),((E-min (L~ z)) .. z)) as S-Sequence_in_R2 by A4, A26, Th37;
A28: z /. ((W-max (L~ z)) .. z) =
z . ((W-max (L~ z)) .. z)
by A12, PARTFUN1:def 6
.=
W-max (L~ z)
by A11, FINSEQ_4:19
;
then
h /. 1 = W-max (L~ z)
by A12, A6, Th8;
then A29:
(h /. 1) `1 = W-bound (L~ z)
by EUCLID:52;
( h is_in_the_area_of z & h /. (len h) = z /. ((E-min (L~ z)) .. z) )
by A12, A6, Th9, Th21, Th22;
then A30:
( len h >= 2 & h is_a_h.c._for z )
by A8, A29, TOPREAL1:def 8;
W-max (L~ z) <> W-min (L~ z)
by Th58;
then
(W-min (L~ z)) .. z > (W-max (L~ z)) .. z
by A3, A28, A16, XXREAL_0:1;
then A31:
L~ M misses L~ h
by A17, A4, A26, Th50;
per cases
( SW-corner (L~ z) = W-min (L~ z) or SW-corner (L~ z) <> W-min (L~ z) )
;
suppose A32:
SW-corner (L~ z) = W-min (L~ z)
;
contradictionA33:
(M /. (len M)) `2 = N-bound (L~ z)
by A10, A25, EUCLID:52;
(M /. 1) `2 = S-bound (L~ z)
by A16, A22, A32, EUCLID:52;
then
M is_a_v.c._for z
by A24, A33;
hence
contradiction
by A30, A31, A23, A19, Th29;
verum end; suppose
SW-corner (L~ z) <> W-min (L~ z)
;
contradictionthen reconsider g =
<*(SW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A15, A16, A21, Th67;
g /. 1
= SW-corner (L~ z)
by FINSEQ_5:15;
then A34:
(g /. 1) `2 = S-bound (L~ z)
by EUCLID:52;
(
len M in dom M &
len g = (len M) + (len <*(SW-corner (L~ z))*>) )
by FINSEQ_1:22, FINSEQ_5:6;
then
g /. (len g) = M /. (len M)
by FINSEQ_4:69;
then A35:
(g /. (len g)) `2 = N-bound (L~ z)
by A10, A25, EUCLID:52;
(LSeg ((M /. 1),(SW-corner (L~ z)))) /\ (L~ h) c= (LSeg ((M /. 1),(SW-corner (L~ z)))) /\ (L~ z)
by A13, A27, A20, A9, JORDAN4:35, XBOOLE_1:26;
then A36:
(LSeg ((M /. 1),(SW-corner (L~ z)))) /\ (L~ h) c= {(M /. 1)}
by A16, A22, PSCOMP_1:35;
(
L~ g = (L~ M) \/ (LSeg ((SW-corner (L~ z)),(M /. 1))) &
M /. 1
in L~ M )
by A23, A19, JORDAN3:1, SPPOL_2:20;
then A37:
L~ g misses L~ h
by A31, A36, ZFMISC_1:125;
<*(SW-corner (L~ z))*> is_in_the_area_of z
by Th28;
then
g is_in_the_area_of z
by A24, Th24;
then
(
len g >= 2 &
g is_a_v.c._for z )
by A34, A35, TOPREAL1:def 8;
hence
contradiction
by A30, A37, Th29;
verum end;