let z be constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = N-min (L~ z) implies (N-max (L~ z)) .. z < (S-max (L~ z)) .. z )
set i1 = (N-max (L~ z)) .. z;
set i2 = (S-max (L~ z)) .. z;
assume that
A1:
z /. 1 = N-min (L~ z)
and
A2:
(N-max (L~ z)) .. z >= (S-max (L~ z)) .. z
; contradiction
A3:
N-min (L~ z) <> N-max (L~ z)
by Th52;
A4:
S-max (L~ z) in rng z
by Th42;
then A5:
(S-max (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A6:
(S-max (L~ z)) .. z <= len z
by FINSEQ_3:25;
A7: z /. ((S-max (L~ z)) .. z) =
z . ((S-max (L~ z)) .. z)
by A5, PARTFUN1:def 6
.=
S-max (L~ z)
by A4, FINSEQ_4:19
;
then A8:
(z /. ((S-max (L~ z)) .. z)) `2 = S-bound (L~ z)
by EUCLID:52;
A9:
1 <= (S-max (L~ z)) .. z
by A5, FINSEQ_3:25;
A10:
(S-max (L~ z)) .. z <> 0
by A5, FINSEQ_3:25;
(z /. 1) `2 = N-bound (L~ z)
by A1, EUCLID:52;
then A11:
(S-max (L~ z)) .. z <> 1
by A8, TOPREAL5:16;
z /. 2 in N-most (L~ z)
by A1, Th30;
then A12: (z /. 2) `2 =
(N-min (L~ z)) `2
by PSCOMP_1:39
.=
N-bound (L~ z)
by EUCLID:52
;
then
(S-max (L~ z)) .. z <> 2
by A8, TOPREAL5:16;
then
(S-max (L~ z)) .. z <> 0 & ... & (S-max (L~ z)) .. z <> 2
by A10, A11;
then A13:
(S-max (L~ z)) .. z > 2
;
then reconsider h = mid (z,((S-max (L~ z)) .. z),2) as S-Sequence_in_R2 by A6, Th37;
A14:
2 <= len z
by NAT_D:60;
then A15:
2 in dom z
by FINSEQ_3:25;
then A16:
(h /. (len h)) `2 = N-bound (L~ z)
by A5, A12, Th9;
h /. 1 = S-max (L~ z)
by A5, A7, A15, Th8;
then A17:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:52;
h is_in_the_area_of z
by A5, A15, Th21, Th22;
then A18:
h is_a_v.c._for z
by A17, A16;
A19:
N-max (L~ z) in rng z
by Th40;
then A20:
(N-max (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A21: z /. ((N-max (L~ z)) .. z) =
z . ((N-max (L~ z)) .. z)
by PARTFUN1:def 6
.=
N-max (L~ z)
by A19, FINSEQ_4:19
;
A22:
(N-max (L~ z)) .. z <= len z
by A20, FINSEQ_3:25;
z /. (len z) = N-min (L~ z)
by A1, FINSEQ_6:def 1;
then A23:
(N-max (L~ z)) .. z < len z
by A22, A21, A3, XXREAL_0:1;
then
((N-max (L~ z)) .. z) + 1 <= len z
by NAT_1:13;
then
(len z) - ((N-max (L~ z)) .. z) >= 1
by XREAL_1:19;
then
(len z) -' ((N-max (L~ z)) .. z) >= 1
by NAT_D:39;
then A24:
((len z) -' ((N-max (L~ z)) .. z)) + 1 >= 1 + 1
by XREAL_1:6;
( (N-max (L~ z)) `2 = N-bound (L~ z) & (S-max (L~ z)) `2 = S-bound (L~ z) )
by EUCLID:52;
then
z /. ((N-max (L~ z)) .. z) <> z /. ((S-max (L~ z)) .. z)
by A7, A21, TOPREAL5:16;
then A25:
(N-max (L~ z)) .. z > (S-max (L~ z)) .. z
by A2, XXREAL_0:1;
then
(N-max (L~ z)) .. z > 1
by A9, XXREAL_0:2;
then reconsider M = mid (z,(len z),((N-max (L~ z)) .. z)) as S-Sequence_in_R2 by A23, Th37;
A26:
1 in dom M
by FINSEQ_5:6;
A27:
len z in dom z
by FINSEQ_5:6;
then A28: M /. (len M) =
z /. ((N-max (L~ z)) .. z)
by A20, Th9
.=
N-max (L~ z)
by A19, FINSEQ_5:38
;
A29:
L~ M misses L~ h
by A22, A25, A13, Th49;
A30:
2 <= len h
by TOPREAL1:def 8;
1 <= (N-max (L~ z)) .. z
by A20, FINSEQ_3:25;
then A31:
len M = ((len z) -' ((N-max (L~ z)) .. z)) + 1
by A22, FINSEQ_6:187;
then A32:
M /. (len M) in L~ M
by A24, JORDAN3:1;
A33:
z /. 1 = z /. (len z)
by FINSEQ_6:def 1;
then A34:
M /. 1 = z /. 1
by A20, A27, Th8;
per cases
( ( NW-corner (L~ z) = N-min (L~ z) & NE-corner (L~ z) = N-max (L~ z) ) or ( NW-corner (L~ z) = N-min (L~ z) & NE-corner (L~ z) <> N-max (L~ z) ) or ( NW-corner (L~ z) <> N-min (L~ z) & NE-corner (L~ z) = N-max (L~ z) ) or ( NW-corner (L~ z) <> N-min (L~ z) & NE-corner (L~ z) <> N-max (L~ z) ) )
;
suppose that A35:
NW-corner (L~ z) = N-min (L~ z)
and A36:
NE-corner (L~ z) = N-max (L~ z)
;
contradictionA37:
(M /. (len M)) `1 = E-bound (L~ z)
by A28, A36, EUCLID:52;
M /. 1
= z /. (len z)
by A20, A27, Th8;
then A38:
(M /. 1) `1 = W-bound (L~ z)
by A1, A33, A35, EUCLID:52;
M is_in_the_area_of z
by A20, A27, Th21, Th22;
then
M is_a_h.c._for z
by A38, A37;
hence
contradiction
by A18, A29, A31, A24, A30, Th29;
verum end; suppose that A39:
NW-corner (L~ z) = N-min (L~ z)
and A40:
NE-corner (L~ z) <> N-max (L~ z)
;
contradictionreconsider g =
M ^ <*(NE-corner (L~ z))*> as
S-Sequence_in_R2 by A20, A21, A27, A40, Th62;
A41:
(
len g >= 2 &
L~ g = (L~ M) \/ (LSeg ((M /. (len M)),(NE-corner (L~ z)))) )
by SPPOL_2:19, TOPREAL1:def 8;
len g =
(len M) + (len <*(NE-corner (L~ z))*>)
by FINSEQ_1:22
.=
(len M) + 1
by FINSEQ_1:39
;
then
g /. (len g) = NE-corner (L~ z)
by FINSEQ_4:67;
then A42:
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:52;
(
M is_in_the_area_of z &
<*(NE-corner (L~ z))*> is_in_the_area_of z )
by A20, A27, Th21, Th22, Th25;
then A43:
g is_in_the_area_of z
by Th24;
(LSeg ((M /. (len M)),(NE-corner (L~ z)))) /\ (L~ h) c= (LSeg ((M /. (len M)),(NE-corner (L~ z)))) /\ (L~ z)
by A9, A6, A14, JORDAN4:35, XBOOLE_1:26;
then A44:
(LSeg ((M /. (len M)),(NE-corner (L~ z)))) /\ (L~ h) c= {(M /. (len M))}
by A28, PSCOMP_1:43;
g /. 1 =
M /. 1
by A26, FINSEQ_4:68
.=
z /. 1
by A20, A27, A33, Th8
;
then
(g /. 1) `1 = W-bound (L~ z)
by A1, A39, EUCLID:52;
then
g is_a_h.c._for z
by A43, A42;
hence
contradiction
by A18, A29, A32, A30, A41, A44, Th29, ZFMISC_1:125;
verum end; suppose that A45:
NW-corner (L~ z) <> N-min (L~ z)
and A46:
NE-corner (L~ z) = N-max (L~ z)
;
contradictionreconsider g =
<*(NW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A1, A20, A27, A33, A45, Th66;
(
len M in dom M &
len g = (len M) + (len <*(NW-corner (L~ z))*>) )
by FINSEQ_1:22, FINSEQ_5:6;
then g /. (len g) =
M /. (len M)
by FINSEQ_4:69
.=
z /. ((N-max (L~ z)) .. z)
by A20, A27, Th9
.=
N-max (L~ z)
by A19, FINSEQ_5:38
;
then A47:
(g /. (len g)) `1 = E-bound (L~ z)
by A46, EUCLID:52;
A48:
(
len g >= 2 &
L~ g = (L~ M) \/ (LSeg ((NW-corner (L~ z)),(M /. 1))) )
by SPPOL_2:20, TOPREAL1:def 8;
g /. 1
= NW-corner (L~ z)
by FINSEQ_5:15;
then A49:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:52;
(LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ h) c= (LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ z)
by A9, A6, A14, JORDAN4:35, XBOOLE_1:26;
then A50:
(LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ h) c= {(M /. 1)}
by A1, A34, PSCOMP_1:43;
A51:
M /. 1
in L~ M
by A31, A24, JORDAN3:1;
(
M is_in_the_area_of z &
<*(NW-corner (L~ z))*> is_in_the_area_of z )
by A20, A27, Th21, Th22, Th26;
then
g is_in_the_area_of z
by Th24;
then
g is_a_h.c._for z
by A49, A47;
hence
contradiction
by A18, A29, A30, A48, A50, A51, Th29, ZFMISC_1:125;
verum end; suppose A52:
(
NW-corner (L~ z) <> N-min (L~ z) &
NE-corner (L~ z) <> N-max (L~ z) )
;
contradictionset K =
<*(NW-corner (L~ z))*> ^ M;
reconsider g =
(<*(NW-corner (L~ z))*> ^ M) ^ <*(NE-corner (L~ z))*> as
S-Sequence_in_R2 by A1, A20, A21, A27, A33, A52, Lm1;
1
in dom (<*(NW-corner (L~ z))*> ^ M)
by FINSEQ_5:6;
then g /. 1 =
(<*(NW-corner (L~ z))*> ^ M) /. 1
by FINSEQ_4:68
.=
NW-corner (L~ z)
by FINSEQ_5:15
;
then A53:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:52;
len g =
(len (<*(NW-corner (L~ z))*> ^ M)) + (len <*(NE-corner (L~ z))*>)
by FINSEQ_1:22
.=
(len (<*(NW-corner (L~ z))*> ^ M)) + 1
by FINSEQ_1:39
;
then
g /. (len g) = NE-corner (L~ z)
by FINSEQ_4:67;
then A54:
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:52;
(
M is_in_the_area_of z &
<*(NW-corner (L~ z))*> is_in_the_area_of z )
by A20, A27, Th21, Th22, Th26;
then A55:
<*(NW-corner (L~ z))*> ^ M is_in_the_area_of z
by Th24;
<*(NE-corner (L~ z))*> is_in_the_area_of z
by Th25;
then
g is_in_the_area_of z
by A55, Th24;
then A56:
g is_a_h.c._for z
by A53, A54;
len (<*(NW-corner (L~ z))*> ^ M) = (len M) + (len <*(NW-corner (L~ z))*>)
by FINSEQ_1:22;
then
len (<*(NW-corner (L~ z))*> ^ M) >= len M
by NAT_1:11;
then
len (<*(NW-corner (L~ z))*> ^ M) >= 2
by A31, A24, XXREAL_0:2;
then A57:
(<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M)) in L~ (<*(NW-corner (L~ z))*> ^ M)
by JORDAN3:1;
(LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ h) c= (LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ z)
by A9, A6, A14, JORDAN4:35, XBOOLE_1:26;
then A58:
(LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ h) c= {(M /. 1)}
by A1, A34, PSCOMP_1:43;
(
L~ (<*(NW-corner (L~ z))*> ^ M) = (L~ M) \/ (LSeg ((NW-corner (L~ z)),(M /. 1))) &
M /. 1
in L~ M )
by A31, A24, JORDAN3:1, SPPOL_2:20;
then A59:
L~ (<*(NW-corner (L~ z))*> ^ M) misses L~ h
by A29, A58, ZFMISC_1:125;
(
len M in dom M &
len (<*(NW-corner (L~ z))*> ^ M) = (len M) + (len <*(NW-corner (L~ z))*>) )
by FINSEQ_1:22, FINSEQ_5:6;
then A60:
(<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M)) =
M /. (len M)
by FINSEQ_4:69
.=
z /. ((N-max (L~ z)) .. z)
by A20, A27, Th9
.=
N-max (L~ z)
by A19, FINSEQ_5:38
;
(LSeg (((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(NE-corner (L~ z)))) /\ (L~ h) c= (LSeg (((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(NE-corner (L~ z)))) /\ (L~ z)
by A9, A6, A14, JORDAN4:35, XBOOLE_1:26;
then A61:
(LSeg (((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(NE-corner (L~ z)))) /\ (L~ h) c= {((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M)))}
by A60, PSCOMP_1:43;
(
len g >= 2 &
L~ g = (L~ (<*(NW-corner (L~ z))*> ^ M)) \/ (LSeg (((<*(NW-corner (L~ z))*> ^ M) /. (len (<*(NW-corner (L~ z))*> ^ M))),(NE-corner (L~ z)))) )
by SPPOL_2:19, TOPREAL1:def 8;
hence
contradiction
by A18, A30, A56, A59, A57, A61, Th29, ZFMISC_1:125;
verum end;