let n be Element of 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 8;
E-bound (L~ (Cage (C,n))) <> W-bound (L~ (Cage (C,n)))
by SPRECT_1:33;
then
p <> (Lower_Seq (C,n)) . 1
by A2, A5, EUCLID:56;
then reconsider g1 = R_Cut ((Lower_Seq (C,n)),p) as being_S-Seq FinSequence of (TOP-REAL 2) by A1, JORDAN3:70;
len g1 in dom g1
by FINSEQ_5:6;
then A6: g1 /. (len g1) =
g1 . (len g1)
by PARTFUN1:def 8
.=
p
by A1, JORDAN3:59
;
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:22, SPRECT_3:63;
then
g1 is_in_the_area_of Cage (C,n)
by A1, JORDAN1E:22, SPRECT_3:69;
then A7:
g is_in_the_area_of Cage (C,n)
by SPRECT_3:68;
A8:
g /. 1 = g1 /. (len g1)
by FINSEQ_5:68;
A9: g /. (len g) =
g /. (len g1)
by FINSEQ_5:def 3
.=
g1 /. 1
by FINSEQ_5:68
;
(g1 /. 1) `1 =
((Lower_Seq (C,n)) /. 1) `1
by A1, SPRECT_3:39
.=
(E-max (L~ (Cage (C,n)))) `1
by JORDAN1F:6
.=
E-bound (L~ (Cage (C,n)))
by EUCLID:56
;
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 8;
A13:
L~ g = L~ g1
by SPPOL_2:22;
len (Cage (C,n)) > 4
by GOBOARD7:36;
then A14:
rng (Cage (C,n)) c= L~ (Cage (C,n))
by SPPOL_2:18, XXREAL_0:2;
now per 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:56;
A18:
(SW-corner (L~ (Cage (C,n)))) `2 = S-bound (L~ (Cage (C,n)))
by EUCLID:56;
then
(SW-corner (L~ (Cage (C,n)))) `2 <= N-bound (L~ (Cage (C,n)))
by SPRECT_1:24;
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:28;
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:88;
A21:
(W-min (L~ (Cage (C,n)))) `1 = (SW-corner (L~ (Cage (C,n)))) `1
by PSCOMP_1:85;
(W-min (L~ (Cage (C,n)))) `2 >= (SW-corner (L~ (Cage (C,n)))) `2
by PSCOMP_1:87;
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:11;
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:57;
then A22:
rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) c= rng (Upper_Seq (C,n))
by FINSEQ_6:125;
rng (Upper_Seq (C,n)) c= rng (Cage (C,n))
by JORDAN1G:47;
then
rng (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) c= rng (Cage (C,n))
by A22, XBOOLE_1:1;
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:56;
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:55;
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:60;
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:102;
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:15;
then A25:
N-bound (L~ (Cage (C,n))) >= (W-max (L~ (Cage (C,n)))) `2
by PSCOMP_1:71;
A26:
<*(SW-corner (L~ (Cage (C,n))))*> is
special
;
A27:
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:21, SPRECT_3:63;
then
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
is_in_the_area_of Cage (
C,
n)
by A27, JORDAN1E:21, SPRECT_3:69;
then A28:
Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))) is_in_the_area_of Cage (
C,
n)
by SPRECT_3:68;
(W-max (L~ (Cage (C,n)))) `2 > (W-min (L~ (Cage (C,n)))) `2
by SPRECT_2:61;
then A29:
N-min (L~ (Cage (C,n))) <> (Upper_Seq (C,n)) . 1
by A12, A25, EUCLID:56;
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 A27, JORDAN3:70;
A30:
Rev RCutUS is
special
;
A31:
(Rev RCutUS) /. (len (Rev RCutUS)) =
(Rev RCutUS) /. (len RCutUS)
by FINSEQ_5:def 3
.=
RCutUS /. 1
by FINSEQ_5:68
.=
(Upper_Seq (C,n)) /. 1
by A27, SPRECT_3:39
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:5
;
then ((Rev RCutUS) /. (len (Rev RCutUS))) `1 =
W-bound (L~ (Cage (C,n)))
by EUCLID:56
.=
(SW-corner (L~ (Cage (C,n)))) `1
by EUCLID:56
.=
(<*(SW-corner (L~ (Cage (C,n))))*> /. 1) `1
by FINSEQ_4:25
;
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, A26, FINSEQ_3:98, GOBOARD2:13;
set h =
Rev h1;
A32:
Rev h1 is
special
by SPPOL_2:42;
<*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:32;
then
h1 is_in_the_area_of Cage (
C,
n)
by A28, SPRECT_2:28;
then A33:
Rev h1 is_in_the_area_of Cage (
C,
n)
by SPRECT_3:68;
L~ (Rev h1) = L~ h1
by SPPOL_2:22;
then A34:
L~ (Rev h1) = (L~ (Rev RCutUS)) \/ (LSeg (((Rev RCutUS) /. (len (Rev RCutUS))),(SW-corner (L~ (Cage (C,n))))))
by SPPOL_2:19;
A35:
(Index ((N-min (L~ (Cage (C,n)))),(Upper_Seq (C,n)))) + 1
>= 0 + 1
by XREAL_1:9;
A36:
2
<= len g
by TOPREAL1:def 10;
len h1 =
(len (Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))))) + 1
by FINSEQ_2:19
.=
(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 A27, A29, JORDAN3:60
;
then
len h1 >= 1
+ 1
by A35, XREAL_1:9;
then A37:
len (Rev h1) >= 2
by FINSEQ_5:def 3;
A38:
(Rev h1) /. 1
= h1 /. (len h1)
by FINSEQ_5:68;
A39:
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:83
.=
(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:68
.=
N-min (L~ (Cage (C,n)))
by A27, Th45
;
then A40:
(h1 /. 1) `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:56;
A41:
(h1 /. (len h1)) `2 =
(h1 /. ((len (Rev (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n)))))))) + 1)) `2
by FINSEQ_2:19
.=
(SW-corner (L~ (Cage (C,n)))) `2
by FINSEQ_4:82
.=
S-bound (L~ (Cage (C,n)))
by EUCLID:56
;
A42:
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:68
;
then
Rev h1 is_a_v.c._for Cage (
C,
n)
by A33, A40, A38, A41, SPRECT_2:def 3;
then
L~ g meets L~ (Rev h1)
by A10, A32, A36, A37, SPRECT_2:33;
then consider x being
set such that A43:
x in L~ g
and A44:
x in L~ (Rev h1)
by XBOOLE_0:3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A43;
A45:
L~ RCutUS c= L~ (Upper_Seq (C,n))
by Th7, JORDAN3:76;
A46:
L~ g c= L~ (Lower_Seq (C,n))
by A1, A13, JORDAN3:76;
then A47:
x in L~ (Lower_Seq (C,n))
by A43;
now per cases
( x in L~ (Rev RCutUS) or x in LSeg (((Rev RCutUS) /. (len (Rev RCutUS))),(SW-corner (L~ (Cage (C,n))))) )
by A44, A34, XBOOLE_0:def 3;
suppose
x in L~ (Rev RCutUS)
;
contradictionthen A48:
x in L~ RCutUS
by SPPOL_2:22;
then
x in (L~ (Lower_Seq (C,n))) /\ (L~ (Upper_Seq (C,n)))
by A43, A46, A45, XBOOLE_0:def 4;
then A49:
x in {(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
by JORDAN1E:20;
now per cases
( x = E-max (L~ (Cage (C,n))) or x = W-min (L~ (Cage (C,n))) )
by A49, 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 A48, 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 A39, PARTFUN1:def 8;
then
(Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A27, Th43;
then
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A39, PARTFUN1:def 8;
then A50:
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:13;
then A51:
E-bound (L~ (Cage (C,n))) >= (N-max (L~ (Cage (C,n)))) `1
by PSCOMP_1:71;
(N-max (L~ (Cage (C,n)))) `1 > (N-min (L~ (Cage (C,n)))) `1
by SPRECT_2:55;
hence
contradiction
by A50, A51, EUCLID:56;
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, A43, JORDAN1F:8;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A42, PARTFUN1:def 8;
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 A42, PARTFUN1:def 8;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end; suppose A52:
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:87;
then A53:
(W-min (L~ (Cage (C,n)))) `2 >= x `2
by A31, A52, TOPREAL1:10;
A54:
(W-min (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:56;
(SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:56;
then A55:
x `1 = W-bound (L~ (Cage (C,n)))
by A31, A52, A54, GOBOARD7:5;
L~ (Cage (C,n)) = (L~ (Lower_Seq (C,n))) \/ (L~ (Upper_Seq (C,n)))
by JORDAN1E:17;
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 A47, A55, SPRECT_2:16;
then
x `2 >= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:88;
then
x `2 = (W-min (L~ (Cage (C,n)))) `2
by A53, XXREAL_0:1;
then
x = W-min (L~ (Cage (C,n)))
by A54, A55, TOPREAL3:11;
then
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A13, A43, JORDAN1F:8;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A42, PARTFUN1:def 8;
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 A42, PARTFUN1:def 8;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end; suppose A56:
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)))));
A57:
2
<= len g
by TOPREAL1:def 10;
W-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:15;
then A58:
N-bound (L~ (Cage (C,n))) >= (W-max (L~ (Cage (C,n)))) `2
by PSCOMP_1:71;
A59:
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:21, SPRECT_3:63;
then A60:
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
is_in_the_area_of Cage (
C,
n)
by A59, JORDAN1E:21, SPRECT_3:69;
(W-max (L~ (Cage (C,n)))) `2 > (W-min (L~ (Cage (C,n)))) `2
by SPRECT_2:61;
then
N-min (L~ (Cage (C,n))) <> (Upper_Seq (C,n)) . 1
by A12, A58, EUCLID:56;
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 A59, JORDAN3:70;
A61:
len RCutUS >= 2
by TOPREAL1:def 10;
(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 A59, Th45;
then A62:
((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:56;
RCutUS /. 1 =
(Upper_Seq (C,n)) /. 1
by A59, SPRECT_3:39
.=
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 A56, EUCLID:56;
then
R_Cut (
(Upper_Seq (C,n)),
(N-min (L~ (Cage (C,n)))))
is_a_v.c._for Cage (
C,
n)
by A60, A62, SPRECT_2:def 3;
then
L~ g meets L~ (R_Cut ((Upper_Seq (C,n)),(N-min (L~ (Cage (C,n))))))
by A10, A57, A61, SPRECT_2:33;
then consider x being
set such that A63:
x in L~ g
and A64:
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 A63;
A65:
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n))
by FINSEQ_5:6;
A66:
L~ g c= L~ (Lower_Seq (C,n))
by A1, A13, JORDAN3:76;
A67:
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:76;
then
x in (L~ (Lower_Seq (C,n))) /\ (L~ (Upper_Seq (C,n)))
by A63, A64, A66, XBOOLE_0:def 4;
then A68:
x in {(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))}
by JORDAN1E:20;
now per cases
( x = E-max (L~ (Cage (C,n))) or x = W-min (L~ (Cage (C,n))) )
by A68, 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 A64, 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 A67, PARTFUN1:def 8;
then
(Upper_Seq (C,n)) . (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A59, Th43;
then
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by A67, PARTFUN1:def 8;
then A69:
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:13;
then A70:
E-bound (L~ (Cage (C,n))) >= (N-max (L~ (Cage (C,n)))) `1
by PSCOMP_1:71;
(N-max (L~ (Cage (C,n)))) `1 > (N-min (L~ (Cage (C,n)))) `1
by SPRECT_2:55;
hence
contradiction
by A69, A70, EUCLID:56;
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, A63, JORDAN1F:8;
then
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) in L~ (R_Cut ((Lower_Seq (C,n)),p))
by A65, PARTFUN1:def 8;
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 A65, PARTFUN1:def 8;
hence
contradiction
by A3, JORDAN1F:8;
verum end; hence
contradiction
;
verum end;
hence
contradiction
; verum