let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) holds
p = W-min (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) holds
p = W-min (L~ (Cage (C,n)))
let p be Point of (TOP-REAL 2); ( p in L~ (Lower_Seq (C,n)) & p `1 = W-bound (L~ (Cage (C,n))) implies p = W-min (L~ (Cage (C,n))) )
set Ca = Cage (C,n);
set LS = Lower_Seq (C,n);
set US = Upper_Seq (C,n);
set Emax = E-max (L~ (Cage (C,n)));
set Nmin = N-min (L~ (Cage (C,n)));
set Nmax = N-max (L~ (Cage (C,n)));
set Wmax = W-max (L~ (Cage (C,n)));
set Wmin = W-min (L~ (Cage (C,n)));
set Ebo = E-bound (L~ (Cage (C,n)));
set Sbo = S-bound (L~ (Cage (C,n)));
set Wbo = W-bound (L~ (Cage (C,n)));
set Nbo = N-bound (L~ (Cage (C,n)));
set SW = SW-corner (L~ (Cage (C,n)));
assume that
A1:
p in L~ (Lower_Seq (C,n))
and
A2:
p `1 = W-bound (L~ (Cage (C,n)))
and
A3:
p <> W-min (L~ (Cage (C,n)))
; contradiction
A4:
(Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))
by JORDAN1F:6;
1 in dom (Lower_Seq (C,n))
by FINSEQ_5:6;
then A5:
(Lower_Seq (C,n)) . 1 = E-max (L~ (Cage (C,n)))
by A4, PARTFUN1:def 6;
E-bound (L~ (Cage (C,n))) <> W-bound (L~ (Cage (C,n)))
by SPRECT_1:31;
then
p <> (Lower_Seq (C,n)) . 1
by A2, A5, EUCLID:52;
then reconsider g1 = R_Cut ((Lower_Seq (C,n)),p) as being_S-Seq FinSequence of (TOP-REAL 2) by A1, JORDAN3:35;
len g1 in dom g1
by FINSEQ_5:6;
then A6: g1 /. (len g1) =
g1 . (len g1)
by PARTFUN1:def 6
.=
p
by A1, JORDAN3:24
;
reconsider g = Rev g1 as being_S-Seq FinSequence of (TOP-REAL 2) ;
<*p*> is_in_the_area_of Cage (C,n)
by A1, JORDAN1E:18, SPRECT_3:46;
then
g1 is_in_the_area_of Cage (C,n)
by A1, JORDAN1E:18, SPRECT_3:52;
then A7:
g is_in_the_area_of Cage (C,n)
by SPRECT_3:51;
A8:
g /. 1 = g1 /. (len g1)
by FINSEQ_5:65;
A9: g /. (len g) =
g /. (len g1)
by FINSEQ_5:def 3
.=
g1 /. 1
by FINSEQ_5:65
;
(g1 /. 1) `1 =
((Lower_Seq (C,n)) /. 1) `1
by A1, SPRECT_3:22
.=
(E-max (L~ (Cage (C,n)))) `1
by JORDAN1F:6
.=
E-bound (L~ (Cage (C,n)))
by EUCLID:52
;
then A10:
g is_a_h.c._for Cage (C,n)
by A2, A7, A8, A9, A6, SPRECT_2:def 2;
A11:
(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
1 in dom (Upper_Seq (C,n))
by FINSEQ_5:6;
then A12:
(Upper_Seq (C,n)) . 1 = W-min (L~ (Cage (C,n)))
by A11, PARTFUN1:def 6;
A13:
L~ g = L~ g1
by SPPOL_2:22;
len (Cage (C,n)) > 4
by GOBOARD7:34;
then A14:
rng (Cage (C,n)) c= L~ (Cage (C,n))
by SPPOL_2:18, XXREAL_0:2;
now contradictionper cases
( W-min (L~ (Cage (C,n))) <> SW-corner (L~ (Cage (C,n))) or W-min (L~ (Cage (C,n))) = SW-corner (L~ (Cage (C,n))) )
;
suppose A15:
W-min (L~ (Cage (C,n))) <> SW-corner (L~ (Cage (C,n)))
;
contradictionA16:
not
SW-corner (L~ (Cage (C,n))) in rng (Cage (C,n))
proof
A17:
(SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
A18:
(SW-corner (L~ (Cage (C,n)))) `2 = S-bound (L~ (Cage (C,n)))
by EUCLID:52;
then
(SW-corner (L~ (Cage (C,n)))) `2 <= N-bound (L~ (Cage (C,n)))
by SPRECT_1:22;
then
SW-corner (L~ (Cage (C,n))) in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = W-bound (L~ (Cage (C,n))) & p1 `2 <= N-bound (L~ (Cage (C,n))) & p1 `2 >= S-bound (L~ (Cage (C,n))) ) }
by A17, A18;
then A19:
SW-corner (L~ (Cage (C,n))) in LSeg (
(SW-corner (L~ (Cage (C,n)))),
(NW-corner (L~ (Cage (C,n)))))
by SPRECT_1:26;
assume
SW-corner (L~ (Cage (C,n))) in rng (Cage (C,n))
;
contradiction
then
SW-corner (L~ (Cage (C,n))) in (LSeg ((SW-corner (L~ (Cage (C,n)))),(NW-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n)))
by A14, A19, XBOOLE_0:def 4;
then A20:
(SW-corner (L~ (Cage (C,n)))) `2 >= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:31;
A21:
(W-min (L~ (Cage (C,n)))) `1 = (SW-corner (L~ (Cage (C,n)))) `1
by PSCOMP_1:29;
(W-min (L~ (Cage (C,n)))) `2 >= (SW-corner (L~ (Cage (C,n)))) `2
by PSCOMP_1:30;
then
(W-min (L~ (Cage (C,n)))) `2 = (SW-corner (L~ (Cage (C,n)))) `2
by A20, XXREAL_0:1;
hence
contradiction
by A15, A21, TOPREAL3:6;
verum
end;
N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by Th7;
then
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
= mid (
(Upper_Seq (C,n)),1,
((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))))
by JORDAN1G:49;
then A22:
rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) c= rng (Upper_Seq (C,n))
by FINSEQ_6:119;
rng (Upper_Seq (C,n)) c= rng (Cage (C,n))
by JORDAN1G:39;
then
rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) c= rng (Cage (C,n))
by A22;
then
not
SW-corner (L~ (Cage (C,n))) in rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A16;
then
rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) misses {(SW-corner (L~ (Cage (C,n))))}
by ZFMISC_1:50;
then
rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) misses rng <*(SW-corner (L~ (Cage (C,n))))*>
by FINSEQ_1:38;
then A23:
rng (Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))) misses rng <*(SW-corner (L~ (Cage (C,n))))*>
by FINSEQ_5:57;
set h1 =
(Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>;
A24:
<*(SW-corner (L~ (Cage (C,n))))*> is
one-to-one
by FINSEQ_3:93;
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:13;
then A25:
N-bound (L~ (Cage (C,n))) >= (W-max (L~ (Cage (C,n)))) `2
by PSCOMP_1:24;
A26:
N-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
by Th7;
then
<*(N-min (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by JORDAN1E:17, SPRECT_3:46;
then
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
is_in_the_area_of Cage (
C,
n)
by A26, JORDAN1E:17, SPRECT_3:52;
then A27:
Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) is_in_the_area_of Cage (
C,
n)
by SPRECT_3:51;
(W-max (L~ (Cage (C,n)))) `2 > (W-min (L~ (Cage (C,n)))) `2
by SPRECT_2:57;
then A28:
N-min (L~ (Cage (C,n))) <> (Upper_Seq (C,n)) . 1
by A12, A25, EUCLID:52;
then reconsider RCutUS =
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n))))) as
being_S-Seq FinSequence of
(TOP-REAL 2) by A26, JORDAN3:35;
A29:
(Rev RCutUS) /. (len (Rev RCutUS)) =
(Rev RCutUS) /. (len RCutUS)
by FINSEQ_5:def 3
.=
RCutUS /. 1
by FINSEQ_5:65
.=
(Upper_Seq (C,n)) /. 1
by A26, SPRECT_3:22
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:5
;
then ((Rev RCutUS) /. (len (Rev RCutUS))) `1 =
W-bound (L~ (Cage (C,n)))
by EUCLID:52
.=
(SW-corner (L~ (Cage (C,n)))) `1
by EUCLID:52
.=
(<*(SW-corner (L~ (Cage (C,n))))*> /. 1) `1
by FINSEQ_4:16
;
then reconsider h1 =
(Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))) ^ <*(SW-corner (L~ (Cage (C,n))))*> as
one-to-one special FinSequence of
(TOP-REAL 2) by A23, A24, FINSEQ_3:91, GOBOARD2:8;
set h =
Rev h1;
A30:
Rev h1 is
special
by SPPOL_2:40;
<*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:28;
then
h1 is_in_the_area_of Cage (
C,
n)
by A27, SPRECT_2:24;
then A31:
Rev h1 is_in_the_area_of Cage (
C,
n)
by SPRECT_3:51;
L~ (Rev h1) = L~ h1
by SPPOL_2:22;
then A32:
L~ (Rev h1) = (L~ (Rev RCutUS)) \/ (LSeg (((Rev RCutUS) /. (len (Rev RCutUS))),(SW-corner (L~ (Cage (C,n))))))
by SPPOL_2:19;
A33:
(Index ((N-min (L~ (Cage (C,n)))),(Upper_Seq (C,n)))) + 1
>= 0 + 1
by XREAL_1:7;
A34:
2
<= len g
by TOPREAL1:def 8;
len h1 =
(len (Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))))) + 1
by FINSEQ_2:16
.=
(len (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))) + 1
by FINSEQ_5:def 3
.=
((Index ((N-min (L~ (Cage (C,n)))),(Upper_Seq (C,n)))) + 1) + 1
by A26, A28, JORDAN3:25
;
then
len h1 >= 1
+ 1
by A33, XREAL_1:7;
then A35:
len (Rev h1) >= 2
by FINSEQ_5:def 3;
A36:
(Rev h1) /. 1
= h1 /. (len h1)
by FINSEQ_5:65;
A37:
len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n))
by FINSEQ_5:6;
1
in dom (Rev RCutUS)
by FINSEQ_5:6;
then h1 /. 1 =
(Rev RCutUS) /. 1
by FINSEQ_4:68
.=
(R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) /. (len (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))))
by FINSEQ_5:65
.=
N-min (L~ (Cage (C,n)))
by A26, Th45
;
then A38:
(h1 /. 1) `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:52;
A39:
(h1 /. (len h1)) `2 =
(h1 /. ((len (Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))))) + 1)) `2
by FINSEQ_2:16
.=
(SW-corner (L~ (Cage (C,n)))) `2
by FINSEQ_4:67
.=
S-bound (L~ (Cage (C,n)))
by EUCLID:52
;
A40:
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n))
by FINSEQ_5:6;
(Rev h1) /. (len (Rev h1)) =
(Rev h1) /. (len h1)
by FINSEQ_5:def 3
.=
h1 /. 1
by FINSEQ_5:65
;
then
Rev h1 is_a_v.c._for Cage (
C,
n)
by A31, A38, A36, A39, SPRECT_2:def 3;
then
L~ g meets L~ (Rev h1)
by A10, A30, A34, A35, SPRECT_2:29;
then consider x being
object such that A41:
x in L~ g
and A42:
x in L~ (Rev h1)
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A41;
A43:
L~ RCutUS c= L~ (Upper_Seq (C,n))
by Th7, JORDAN3:41;
A44:
L~ g c= L~ (Lower_Seq (C,n))
by A1, A13, JORDAN3:41;
then A45:
x in L~ (Lower_Seq (C,n))
by A41;
now contradictionper cases
( x in L~ (Rev RCutUS) or x in LSeg (((Rev RCutUS) /. (len (Rev RCutUS))),(SW-corner (L~ (Cage (C,n))))) )
by A42, A32, XBOOLE_0:def 3;
suppose
x in L~ (Rev RCutUS)
;
contradictionthen A46:
x in L~ RCutUS
by SPPOL_2:22;
then
x in (L~ (Lower_Seq (C,n))) /\ (L~ (Upper_Seq (C,n)))
by A41, A44, A43, XBOOLE_0:def 4;
then A47:
x in {(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
by JORDAN1E:16;
now contradictionper cases
( x = E-max (L~ (Cage (C,n))) or x = W-min (L~ (Cage (C,n))) )
by A47, TARSKI:def 2;
suppose
x = E-max (L~ (Cage (C,n)))
;
contradictionthen
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) in L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A46, JORDAN1F:7;
then
(Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) in L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A37, PARTFUN1:def 6;
then
(Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A26, Th43;
then
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A37, PARTFUN1:def 6;
then A48:
E-max (L~ (Cage (C,n))) = N-min (L~ (Cage (C,n)))
by JORDAN1F:7;
N-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:11;
then A49:
E-bound (L~ (Cage (C,n))) >= (N-max (L~ (Cage (C,n)))) `1
by PSCOMP_1:24;
(N-max (L~ (Cage (C,n)))) `1 > (N-min (L~ (Cage (C,n)))) `1
by SPRECT_2:51;
hence
contradiction
by A48, A49, EUCLID:52;
verum end; suppose
x = W-min (L~ (Cage (C,n)))
;
contradictionthen
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A13, A41, JORDAN1F:8;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A40, PARTFUN1:def 6;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) = p
by A1, Th43;
then
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = p
by A40, PARTFUN1:def 6;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end; suppose A50:
x in LSeg (
((Rev RCutUS) /. (len (Rev RCutUS))),
(SW-corner (L~ (Cage (C,n)))))
;
contradiction
(W-min (L~ (Cage (C,n)))) `2 >= (SW-corner (L~ (Cage (C,n)))) `2
by PSCOMP_1:30;
then A51:
(W-min (L~ (Cage (C,n)))) `2 >= x `2
by A29, A50, TOPREAL1:4;
A52:
(W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
(SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
then A53:
x `1 = W-bound (L~ (Cage (C,n)))
by A29, A50, A52, GOBOARD7:5;
L~ (Cage (C,n)) = (L~ (Lower_Seq (C,n))) \/ (L~ (Upper_Seq (C,n)))
by JORDAN1E:13;
then
L~ (Lower_Seq (C,n)) c= L~ (Cage (C,n))
by XBOOLE_1:7;
then
x in W-most (L~ (Cage (C,n)))
by A45, A53, SPRECT_2:12;
then
x `2 >= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:31;
then
x `2 = (W-min (L~ (Cage (C,n)))) `2
by A51, XXREAL_0:1;
then
x = W-min (L~ (Cage (C,n)))
by A52, A53, TOPREAL3:6;
then
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A13, A41, JORDAN1F:8;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A40, PARTFUN1:def 6;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) = p
by A1, Th43;
then
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = p
by A40, PARTFUN1:def 6;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end; suppose A54:
W-min (L~ (Cage (C,n))) = SW-corner (L~ (Cage (C,n)))
;
contradictionset h =
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))));
A55:
2
<= len g
by TOPREAL1:def 8;
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:13;
then A56:
N-bound (L~ (Cage (C,n))) >= (W-max (L~ (Cage (C,n)))) `2
by PSCOMP_1:24;
A57:
N-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
by Th7;
then
<*(N-min (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by JORDAN1E:17, SPRECT_3:46;
then A58:
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
is_in_the_area_of Cage (
C,
n)
by A57, JORDAN1E:17, SPRECT_3:52;
(W-max (L~ (Cage (C,n)))) `2 > (W-min (L~ (Cage (C,n)))) `2
by SPRECT_2:57;
then
N-min (L~ (Cage (C,n))) <> (Upper_Seq (C,n)) . 1
by A12, A56, EUCLID:52;
then reconsider RCutUS =
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n))))) as
being_S-Seq FinSequence of
(TOP-REAL 2) by A57, JORDAN3:35;
A59:
len RCutUS >= 2
by TOPREAL1:def 8;
(R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) /. (len (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))) = N-min (L~ (Cage (C,n)))
by A57, Th45;
then A60:
((R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) /. (len (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))))) `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:52;
RCutUS /. 1 =
(Upper_Seq (C,n)) /. 1
by A57, SPRECT_3:22
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:5
;
then
((R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) /. 1) `2 = S-bound (L~ (Cage (C,n)))
by A54, EUCLID:52;
then
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
is_a_v.c._for Cage (
C,
n)
by A58, A60, SPRECT_2:def 3;
then
L~ g meets L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A10, A55, A59, SPRECT_2:29;
then consider x being
object such that A61:
x in L~ g
and A62:
x in L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A61;
A63:
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n))
by FINSEQ_5:6;
A64:
L~ g c= L~ (Lower_Seq (C,n))
by A1, A13, JORDAN3:41;
A65:
len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n))
by FINSEQ_5:6;
L~ RCutUS c= L~ (Upper_Seq (C,n))
by Th7, JORDAN3:41;
then
x in (L~ (Lower_Seq (C,n))) /\ (L~ (Upper_Seq (C,n)))
by A61, A62, A64, XBOOLE_0:def 4;
then A66:
x in {(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
by JORDAN1E:16;
now contradictionper cases
( x = E-max (L~ (Cage (C,n))) or x = W-min (L~ (Cage (C,n))) )
by A66, TARSKI:def 2;
suppose
x = E-max (L~ (Cage (C,n)))
;
contradictionthen
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) in L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A62, JORDAN1F:7;
then
(Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) in L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A65, PARTFUN1:def 6;
then
(Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A57, Th43;
then
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A65, PARTFUN1:def 6;
then A67:
E-max (L~ (Cage (C,n))) = N-min (L~ (Cage (C,n)))
by JORDAN1F:7;
N-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:11;
then A68:
E-bound (L~ (Cage (C,n))) >= (N-max (L~ (Cage (C,n)))) `1
by PSCOMP_1:24;
(N-max (L~ (Cage (C,n)))) `1 > (N-min (L~ (Cage (C,n)))) `1
by SPRECT_2:51;
hence
contradiction
by A67, A68, EUCLID:52;
verum end; suppose
x = W-min (L~ (Cage (C,n)))
;
contradictionthen
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A13, A61, JORDAN1F:8;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A63, PARTFUN1:def 6;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) = p
by A1, Th43;
then
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = p
by A63, PARTFUN1:def 6;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end;
hence
contradiction
; verum