let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( 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
; :: thesis: contradiction
A3:
E-max (L~ z) in rng z
by Th50;
A4:
S-max (L~ z) in rng z
by Th46;
A5:
E-min (L~ z) in rng z
by Th49;
A6:
1 in dom z
by FINSEQ_5:6;
A7:
(E-max (L~ z)) .. z in dom z
by A3, FINSEQ_4:30;
then A8:
( 1 <= (E-max (L~ z)) .. z & (E-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A9:
(E-min (L~ z)) .. z in dom z
by A5, FINSEQ_4:30;
then A10:
( 1 <= (E-min (L~ z)) .. z & (E-min (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A11: z /. ((E-min (L~ z)) .. z) =
z . ((E-min (L~ z)) .. z)
by A9, PARTFUN1:def 8
.=
E-min (L~ z)
by A5, FINSEQ_4:29
;
A12:
z /. (len z) = N-min (L~ z)
by A1, FINSEQ_6:def 1;
A13: z /. ((E-max (L~ z)) .. z) =
z . ((E-max (L~ z)) .. z)
by A7, PARTFUN1:def 8
.=
E-max (L~ z)
by A3, FINSEQ_4:29
;
(E-min (L~ z)) `2 < (E-max (L~ z)) `2
by Th57;
then A14:
(E-max (L~ z)) .. z > (E-min (L~ z)) .. z
by A2, A11, A13, XXREAL_0:1;
then A15:
(E-max (L~ z)) .. z > 1
by A10, XXREAL_0:2;
A16:
(S-max (L~ z)) .. z in dom z
by A4, FINSEQ_4:30;
then A17:
( 1 <= (S-max (L~ z)) .. z & (S-max (L~ z)) .. z <= len z )
by FINSEQ_3:27;
A18:
(E-min (L~ z)) .. z < len z
by A8, A14, XXREAL_0:2;
A19: z /. ((S-max (L~ z)) .. z) =
z . ((S-max (L~ z)) .. z)
by A16, PARTFUN1:def 8
.=
S-max (L~ z)
by A4, FINSEQ_4:29
;
A20:
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
by A1, Lm7;
then reconsider h = mid z,((S-max (L~ z)) .. z),((E-max (L~ z)) .. z) as S-Sequence_in_R2 by A15, A17, Th41;
A21:
h is_in_the_area_of z
by A7, A16, Th25, Th26;
h /. 1 = S-max (L~ z)
by A7, A16, A19, Th12;
then A22:
(h /. 1) `2 = S-bound (L~ z)
by EUCLID:56;
A23:
h /. (len h) = z /. ((E-max (L~ z)) .. z)
by A7, A16, Th13;
A24:
S-bound (L~ z) < N-bound (L~ z)
by TOPREAL5:22;
( (N-min (L~ z)) `2 = N-bound (L~ z) & (S-max (L~ z)) `2 = S-bound (L~ z) )
by EUCLID:56;
then A25:
(S-max (L~ z)) .. z < len z
by A12, A17, A19, A24, XXREAL_0:1;
N-max (L~ z) in L~ z
by SPRECT_1:13;
then
(N-max (L~ z)) `1 <= E-bound (L~ z)
by PSCOMP_1:71;
then
(N-min (L~ z)) `1 < E-bound (L~ z)
by Th55, XXREAL_0:2;
then
(N-min (L~ z)) `1 < (E-min (L~ z)) `1
by EUCLID:56;
then A26:
(E-min (L~ z)) .. z > 1
by A1, A10, A11, XXREAL_0:1;
then reconsider M = mid z,1,((E-min (L~ z)) .. z) as S-Sequence_in_R2 by A18, Th42;
A27:
L~ M misses L~ h
by A10, A14, A20, A25, Th52;
A28:
1 <= len z
by A10, XXREAL_0:2;
A29: M /. (len M) =
z /. ((E-min (L~ z)) .. z)
by A6, A9, Th13
.=
E-min (L~ z)
by A5, FINSEQ_5:41
;
len M =
(((E-min (L~ z)) .. z) -' 1) + 1
by A10, JORDAN4:20
.=
(E-min (L~ z)) .. z
by A10, XREAL_1:237
;
then A30:
len M >= 1 + 1
by A26, NAT_1:13;
A31:
len h >= 1
by A7, A16, Th9;
len h <> 1
by A7, A16, A20, Th10;
then
len h > 1
by A31, XXREAL_0:1;
then A32:
len h >= 1 + 1
by NAT_1:13;
A33:
M /. 1 = z /. 1
by A6, A9, Th12;
A34:
M is_in_the_area_of z
by A6, A9, Th25, Th26;
A35:
(M /. (len M)) `1 = E-bound (L~ z)
by A29, EUCLID:56;
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 A36:
NW-corner (L~ z) = N-min (L~ z)
and A37:
NE-corner (L~ z) = E-max (L~ z)
;
:: thesis: contradiction
(h /. (len h)) `2 = N-bound (L~ z)
by A13, A23, A37, EUCLID:56;
then A38:
h is_a_v.c._for z
by A21, A22, Def3;
(M /. 1) `1 = W-bound (L~ z)
by A1, A33, A36, EUCLID:56;
then
M is_a_h.c._for z
by A34, A35, Def2;
hence
contradiction
by A27, A30, A32, A38, Th33;
:: thesis: verum end; suppose that A39:
NW-corner (L~ z) <> N-min (L~ z)
and A40:
NE-corner (L~ z) = E-max (L~ z)
;
:: thesis: contradiction
(h /. (len h)) `2 = N-bound (L~ z)
by A13, A23, A40, EUCLID:56;
then A41:
h is_a_v.c._for z
by A21, A22, Def3;
reconsider g =
<*(NW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A1, A6, A9, A39, Th70;
A42:
2
<= len g
by TOPREAL1:def 10;
<*(NW-corner (L~ z))*> is_in_the_area_of z
by Th30;
then A43:
g is_in_the_area_of z
by A34, Th28;
g /. 1
= NW-corner (L~ z)
by FINSEQ_5:16;
then A44:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
A45:
len M in dom M
by FINSEQ_5:6;
len g = (len M) + (len <*(NW-corner (L~ z))*>)
by FINSEQ_1:35;
then g /. (len g) =
M /. (len M)
by A45, FINSEQ_4:84
.=
z /. ((E-min (L~ z)) .. z)
by A6, A9, Th13
.=
E-min (L~ z)
by A5, FINSEQ_5:41
;
then
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:56;
then A46:
g is_a_h.c._for z
by A43, A44, Def2;
A47:
L~ g = (L~ M) \/ (LSeg (NW-corner (L~ z)),(M /. 1))
by SPPOL_2:20;
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= (LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ z)
by A8, A17, JORDAN4:47, XBOOLE_1:26;
then A48:
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h) c= {(M /. 1)}
by A1, A33, PSCOMP_1:102;
M /. 1
in L~ M
by A30, JORDAN3:34;
hence
contradiction
by A27, A32, A41, A42, A46, A47, A48, Th33, ZFMISC_1:149;
:: thesis: verum end; suppose that A49:
NW-corner (L~ z) = N-min (L~ z)
and A50:
NE-corner (L~ z) <> E-max (L~ z)
;
:: thesis: contradiction
M /. 1
= z /. 1
by A6, A9, Th12;
then
(M /. 1) `1 = W-bound (L~ z)
by A1, A49, EUCLID:56;
then A51:
M is_a_h.c._for z
by A34, A35, Def2;
reconsider N =
h ^ <*(NE-corner (L~ z))*> as
S-Sequence_in_R2 by A7, A13, A16, A50, Th69;
A52:
(
len M >= 2 &
len N >= 2 )
by TOPREAL1:def 10;
<*(NE-corner (L~ z))*> is_in_the_area_of z
by Th29;
then A53:
N is_in_the_area_of z
by A21, Th28;
1
in dom h
by FINSEQ_5:6;
then A54:
(N /. 1) `2 = S-bound (L~ z)
by A22, FINSEQ_4:83;
len N =
(len h) + (len <*(NE-corner (L~ z))*>)
by FINSEQ_1:35
.=
(len h) + 1
by FINSEQ_1:56
;
then
N /. (len N) = NE-corner (L~ z)
by FINSEQ_4:82;
then
(N /. (len N)) `2 = N-bound (L~ z)
by EUCLID:56;
then A55:
N is_a_v.c._for z
by A53, A54, Def3;
A56:
L~ N = (L~ h) \/ (LSeg (NE-corner (L~ z)),(h /. (len h)))
by SPPOL_2:19;
(LSeg (h /. (len h)),(NE-corner (L~ z))) /\ (L~ M) c= (LSeg (h /. (len h)),(NE-corner (L~ z))) /\ (L~ z)
by A10, A28, JORDAN4:47, XBOOLE_1:26;
then A57:
(LSeg (h /. (len h)),(NE-corner (L~ z))) /\ (L~ M) c= {(h /. (len h))}
by A13, A23, PSCOMP_1:112;
h /. (len h) in L~ h
by A32, JORDAN3:34;
then
L~ M misses L~ N
by A27, A56, A57, ZFMISC_1:149;
hence
contradiction
by A51, A52, A55, Th33;
:: thesis: verum end; suppose that A58:
NW-corner (L~ z) <> N-min (L~ z)
and A59:
NE-corner (L~ z) <> E-max (L~ z)
;
:: thesis: contradictionreconsider g =
<*(NW-corner (L~ z))*> ^ M as
S-Sequence_in_R2 by A1, A6, A9, A58, Th70;
<*(NW-corner (L~ z))*> is_in_the_area_of z
by Th30;
then A60:
g is_in_the_area_of z
by A34, Th28;
g /. 1
= NW-corner (L~ z)
by FINSEQ_5:16;
then A61:
(g /. 1) `1 = W-bound (L~ z)
by EUCLID:56;
A62:
len M in dom M
by FINSEQ_5:6;
len g = (len M) + (len <*(NW-corner (L~ z))*>)
by FINSEQ_1:35;
then g /. (len g) =
M /. (len M)
by A62, FINSEQ_4:84
.=
z /. ((E-min (L~ z)) .. z)
by A6, A9, Th13
.=
E-min (L~ z)
by A5, FINSEQ_5:41
;
then
(g /. (len g)) `1 = E-bound (L~ z)
by EUCLID:56;
then A63:
g is_a_h.c._for z
by A60, A61, Def2;
reconsider N =
h ^ <*(NE-corner (L~ z))*> as
S-Sequence_in_R2 by A7, A13, A16, A59, Th69;
A64:
(
len g >= 2 &
len N >= 2 )
by TOPREAL1:def 10;
<*(NE-corner (L~ z))*> is_in_the_area_of z
by Th29;
then A65:
N is_in_the_area_of z
by A21, Th28;
1
in dom h
by FINSEQ_5:6;
then A66:
(N /. 1) `2 = S-bound (L~ z)
by A22, FINSEQ_4:83;
len N =
(len h) + (len <*(NE-corner (L~ z))*>)
by FINSEQ_1:35
.=
(len h) + 1
by FINSEQ_1:56
;
then
N /. (len N) = NE-corner (L~ z)
by FINSEQ_4:82;
then
(N /. (len N)) `2 = N-bound (L~ z)
by EUCLID:56;
then A67:
N is_a_v.c._for z
by A65, A66, Def3;
A68:
L~ N = (L~ h) \/ (LSeg (NE-corner (L~ z)),(h /. (len h)))
by SPPOL_2:19;
(LSeg (h /. (len h)),(NE-corner (L~ z))) /\ (L~ M) c= (LSeg (h /. (len h)),(NE-corner (L~ z))) /\ (L~ z)
by A10, A28, JORDAN4:47, XBOOLE_1:26;
then A69:
(LSeg (h /. (len h)),(NE-corner (L~ z))) /\ (L~ M) c= {(h /. (len h))}
by A13, A23, PSCOMP_1:112;
h /. (len h) in L~ h
by A32, JORDAN3:34;
then A70:
L~ M misses L~ N
by A27, A68, A69, ZFMISC_1:149;
A71:
L~ g = (L~ M) \/ (LSeg (NW-corner (L~ z)),(M /. 1))
by SPPOL_2:20;
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (LSeg (NE-corner (L~ z)),(h /. (len h))) = {}
by A1, A13, A23, A33, Lm8;
then (LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ N) =
((LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ h)) \/ {}
by A68, 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 A8, A17, JORDAN4:47, XBOOLE_1:26;
then A72:
(LSeg (M /. 1),(NW-corner (L~ z))) /\ (L~ N) c= {(M /. 1)}
by A1, A33, PSCOMP_1:102;
M /. 1
in L~ M
by A30, JORDAN3:34;
hence
contradiction
by A63, A64, A67, A70, A71, A72, Th33, ZFMISC_1:149;
:: thesis: verum end;