let z be constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = N-min (L~ z) implies (E-max (L~ z)) .. z < (S-max (L~ z)) .. z )
set i1 = (E-max (L~ z)) .. z;
set i2 = (S-max (L~ z)) .. z;
assume that
A1:
z /. 1 = N-min (L~ z)
and
A2:
(E-max (L~ z)) .. z >= (S-max (L~ z)) .. z
; contradiction
A3:
(N-min (L~ z)) `1 < (N-max (L~ z)) `1
by Th51;
z /. 2 in N-most (L~ z)
by A1, Th30;
then A4: (z /. 2) `2 =
(N-min (L~ z)) `2
by PSCOMP_1:39
.=
N-bound (L~ z)
by EUCLID:52
;
E-min (L~ z) in L~ z
by SPRECT_1:14;
then A5:
S-bound (L~ z) <= (E-min (L~ z)) `2
by PSCOMP_1:24;
A6:
S-bound (L~ z) < N-bound (L~ z)
by TOPREAL5:16;
A7:
S-max (L~ z) in rng z
by Th42;
then A8:
(S-max (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A9:
(S-max (L~ z)) .. z <= len z
by FINSEQ_3:25;
A10:
(S-max (L~ z)) .. z <> 0
by A8, FINSEQ_3:25;
A11: z /. ((S-max (L~ z)) .. z) =
z . ((S-max (L~ z)) .. z)
by A8, PARTFUN1:def 6
.=
S-max (L~ z)
by A7, FINSEQ_4:19
;
then A12:
(z /. ((S-max (L~ z)) .. z)) `2 = S-bound (L~ z)
by EUCLID:52;
A13:
1 <= (S-max (L~ z)) .. z
by A8, FINSEQ_3:25;
(z /. 1) `2 = N-bound (L~ z)
by A1, EUCLID:52;
then
(S-max (L~ z)) .. z <> 0 & ... & (S-max (L~ z)) .. z <> 2
by A4, A10, A12, A6;
then A14:
(S-max (L~ z)) .. z > 2
;
then reconsider h = mid (z,((S-max (L~ z)) .. z),2) as S-Sequence_in_R2 by A9, Th37;
A15:
2 <= len z
by NAT_D:60;
then A16:
2 in dom z
by FINSEQ_3:25;
then
h /. 1 = S-max (L~ z)
by A8, A11, Th8;
then A17:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:52;
( h is_in_the_area_of z & h /. (len h) = z /. 2 )
by A8, A16, Th9, Th21, Th22;
then A18:
( len h >= 2 & h is_a_v.c._for z )
by A4, A17, TOPREAL1:def 8;
N-max (L~ z) in L~ z
by SPRECT_1:11;
then A19:
(N-max (L~ z)) `1 <= E-bound (L~ z)
by PSCOMP_1:24;
A20:
E-max (L~ z) in rng z
by Th46;
then A21:
(E-max (L~ z)) .. z in dom z
by FINSEQ_4:20;
then A22: z /. ((E-max (L~ z)) .. z) =
z . ((E-max (L~ z)) .. z)
by PARTFUN1:def 6
.=
E-max (L~ z)
by A20, FINSEQ_4:19
;
A23:
(E-max (L~ z)) .. z <= len z
by A21, FINSEQ_3:25;
z /. (len z) = N-min (L~ z)
by A1, FINSEQ_6:def 1;
then
(E-max (L~ z)) .. z <> len z
by A22, A3, A19, EUCLID:52;
then A24:
(E-max (L~ z)) .. z < len z
by A23, XXREAL_0:1;
then
((E-max (L~ z)) .. z) + 1 <= len z
by NAT_1:13;
then
(len z) - ((E-max (L~ z)) .. z) >= 1
by XREAL_1:19;
then
(len z) -' ((E-max (L~ z)) .. z) >= 1
by NAT_D:39;
then A25:
((len z) -' ((E-max (L~ z)) .. z)) + 1 >= 1 + 1
by XREAL_1:6;
(E-min (L~ z)) `2 < (E-max (L~ z)) `2
by Th53;
then
E-max (L~ z) <> S-max (L~ z)
by A5, EUCLID:52;
then A26:
(E-max (L~ z)) .. z > (S-max (L~ z)) .. z
by A2, A11, A22, XXREAL_0:1;
then
(E-max (L~ z)) .. z > 1
by A13, XXREAL_0:2;
then reconsider M = mid (z,(len z),((E-max (L~ z)) .. z)) as S-Sequence_in_R2 by A24, Th37;
A27:
len M >= 2
by TOPREAL1:def 8;
1 <= (E-max (L~ z)) .. z
by A21, FINSEQ_3:25;
then A28:
len M = ((len z) -' ((E-max (L~ z)) .. z)) + 1
by A23, FINSEQ_6:187;
A29:
len z in dom z
by FINSEQ_5:6;
then A30: M /. (len M) =
z /. ((E-max (L~ z)) .. z)
by A21, Th9
.=
E-max (L~ z)
by A20, FINSEQ_5:38
;
A31:
L~ M misses L~ h
by A23, A26, A14, Th49;
A32:
z /. 1 = z /. (len z)
by FINSEQ_6:def 1;
then A33:
M /. 1 = z /. 1
by A21, A29, Th8;
per cases
( NW-corner (L~ z) = N-min (L~ z) or NW-corner (L~ z) <> N-min (L~ z) )
;
suppose A34:
NW-corner (L~ z) = N-min (L~ z)
;
contradiction
M /. 1
= z /. (len z)
by A21, A29, Th8;
then A35:
(M /. 1) `1 = W-bound (L~ z)
by A1, A32, A34, EUCLID:52;
(
M is_in_the_area_of z &
(M /. (len M)) `1 = E-bound (L~ z) )
by A21, A29, A30, Th21, Th22, EUCLID:52;
then
M is_a_h.c._for z
by A35;
hence
contradiction
by A18, A27, A31, Th29;
verum end; suppose
NW-corner (L~ z) <> N-min (L~ z)
;
contradictionthen reconsider g =
<*(NW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A1, A21, A29, A32, Th66;
A36:
(
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 A37:
(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 A13, A9, A15, JORDAN4:35, XBOOLE_1:26;
then A38:
(LSeg ((M /. 1),(NW-corner (L~ z)))) /\ (L~ h) c= {(M /. 1)}
by A1, A33, PSCOMP_1:43;
(
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 /. ((E-max (L~ z)) .. z)
by A21, A29, Th9
.=
E-max (L~ z)
by A20, FINSEQ_5:38
;
then A39:
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:52;
A40:
M /. 1
in L~ M
by A28, A25, JORDAN3:1;
(
M is_in_the_area_of z &
<*(NW-corner (L~ z))*> is_in_the_area_of z )
by A21, A29, Th21, Th22, Th26;
then
g is_in_the_area_of z
by Th24;
then
g is_a_h.c._for z
by A37, A39;
hence
contradiction
by A18, A31, A36, A38, A40, Th29, ZFMISC_1:125;
verum end;