let z be non constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = N-min (L~ z) & N-max (L~ z) <> E-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set i1 = (N-max (L~ z)) .. z;
set i2 = (E-max (L~ z)) .. z;
set j = (S-max (L~ z)) .. z;
assume that
A1:
z /. 1 = N-min (L~ z)
and
A2:
( N-max (L~ z) <> E-max (L~ z) & (N-max (L~ z)) .. z >= (E-max (L~ z)) .. z )
; contradiction
(N-min (L~ z)) .. z = 1
by A1, FINSEQ_6:47;
then A3:
1 < (E-max (L~ z)) .. z
by A1, Lm4;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-max (L~ z)) `2 = S-bound (L~ z) )
by EUCLID:56;
then A4:
N-min (L~ z) <> S-max (L~ z)
by TOPREAL5:22;
A5:
S-max (L~ z) in rng z
by Th46;
then A6:
(S-max (L~ z)) .. z in dom z
by FINSEQ_4:30;
then A7: z /. ((S-max (L~ z)) .. z) =
z . ((S-max (L~ z)) .. z)
by PARTFUN1:def 8
.=
S-max (L~ z)
by A5, FINSEQ_4:29
;
A8:
(S-max (L~ z)) .. z <= len z
by A6, FINSEQ_3:27;
z /. (len z) = z /. 1
by FINSEQ_6:def 1;
then A9:
(S-max (L~ z)) .. z < len z
by A1, A8, A7, A4, XXREAL_0:1;
A10:
N-max (L~ z) in rng z
by Th44;
then A11:
(N-max (L~ z)) .. z in dom z
by FINSEQ_4:30;
then A12:
1 <= (N-max (L~ z)) .. z
by FINSEQ_3:27;
A13: z /. ((N-max (L~ z)) .. z) =
z . ((N-max (L~ z)) .. z)
by A11, PARTFUN1:def 8
.=
N-max (L~ z)
by A10, FINSEQ_4:29
;
A14:
(S-max (L~ z)) .. z > (N-max (L~ z)) .. z
by A1, Lm5;
then reconsider h = mid z,((S-max (L~ z)) .. z),((N-max (L~ z)) .. z) as S-Sequence_in_R2 by A12, A9, Th41;
h /. 1 = S-max (L~ z)
by A11, A6, A7, Th12;
then A15:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:56;
h /. (len h) = z /. ((N-max (L~ z)) .. z)
by A11, A6, Th13;
then A16:
(h /. (len h)) `2 = N-bound (L~ z)
by A13, EUCLID:56;
h is_in_the_area_of z
by A11, A6, Th25, Th26;
then A17:
h is_a_v.c._for z
by A15, A16, Def3;
A18:
1 <= (S-max (L~ z)) .. z
by A6, FINSEQ_3:27;
A19:
(N-max (L~ z)) .. z <= len z
by A11, FINSEQ_3:27;
A20:
E-max (L~ z) in rng z
by Th50;
then A21:
(E-max (L~ z)) .. z in dom z
by FINSEQ_4:30;
then A22:
( 1 <= (E-max (L~ z)) .. z & (E-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
z /. ((E-max (L~ z)) .. z) =
z . ((E-max (L~ z)) .. z)
by A21, PARTFUN1:def 8
.=
E-max (L~ z)
by A20, FINSEQ_4:29
;
then A23:
(N-max (L~ z)) .. z > (E-max (L~ z)) .. z
by A2, A13, XXREAL_0:1;
then
(E-max (L~ z)) .. z < len z
by A19, XXREAL_0:2;
then reconsider M = mid z,1,((E-max (L~ z)) .. z) as S-Sequence_in_R2 by A3, Th42;
A24:
len M >= 2
by TOPREAL1:def 10;
A25:
1 in dom z
by FINSEQ_5:6;
then A26: M /. (len M) =
z /. ((E-max (L~ z)) .. z)
by A21, Th13
.=
E-max (L~ z)
by A20, FINSEQ_5:41
;
A27:
( len h >= 2 & L~ M misses L~ h )
by A14, A9, A3, A23, Th52, TOPREAL1:def 10;
per cases
( NW-corner (L~ z) = N-min (L~ z) or NW-corner (L~ z) <> N-min (L~ z) )
;
suppose A28:
NW-corner (L~ z) = N-min (L~ z)
;
contradiction
M /. 1
= z /. 1
by A25, A21, Th12;
then A29:
(M /. 1) `1 = W-bound (L~ z)
by A1, A28, EUCLID:56;
(
M is_in_the_area_of z &
(M /. (len M)) `1 = E-bound (L~ z) )
by A25, A21, A26, Th25, Th26, EUCLID:56;
then
M is_a_h.c._for z
by A29, Def2;
hence
contradiction
by A17, A24, A27, Th33;
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, A25, A21, Th70;
A30:
(
len g >= 2 &
L~ g = (L~ M) \/ (LSeg (NW-corner (L~ z)),(M /. 1)) )
by SPPOL_2:20, TOPREAL1:def 10;
g /. 1
= NW-corner (L~ z)
by FINSEQ_5:16;
then A31:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
len M =
(((E-max (L~ z)) .. z) -' 1) + 1
by A22, JORDAN4:20
.=
(E-max (L~ z)) .. z
by A3, XREAL_1:237
;
then
len M >= 1
+ 1
by A3, NAT_1:13;
then A32:
M /. 1
in L~ M
by JORDAN3:34;
(
len M in dom M &
len g = (len M) + (len <*(NW-corner (L~ z))*>) )
by FINSEQ_1:35, FINSEQ_5:6;
then g /. (len g) =
M /. (len M)
by FINSEQ_4:84
.=
z /. ((E-max (L~ z)) .. z)
by A25, A21, Th13
.=
E-max (L~ z)
by A20, FINSEQ_5:41
;
then A33:
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:56;
(
M /. 1
= z /. 1 &
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= (LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ z) )
by A25, A12, A19, A18, A8, A21, Th12, JORDAN4:47, XBOOLE_1:26;
then A34:
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= {(M /. 1)}
by A1, PSCOMP_1:102;
(
M is_in_the_area_of z &
<*(NW-corner (L~ z))*> is_in_the_area_of z )
by A25, A21, Th25, Th26, Th30;
then
g is_in_the_area_of z
by Th28;
then
g is_a_h.c._for z
by A31, A33, Def2;
hence
contradiction
by A17, A27, A30, A34, A32, Th33, ZFMISC_1:149;
verum end;