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