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