let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Upper_Seq (C,n)) /. 2) `1 = W-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ((Upper_Seq (C,n)) /. 2) `1 = W-bound (L~ (Cage (C,n)))
set Ca = Cage (C,n);
set US = Upper_Seq (C,n);
set Wmin = W-min (L~ (Cage (C,n)));
set Emax = E-max (L~ (Cage (C,n)));
set Nmin = N-min (L~ (Cage (C,n)));
E-max (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:46;
then A1:
E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by FINSEQ_6:90, SPRECT_2:43;
len (Upper_Seq (C,n)) >= 3
by JORDAN1E:15;
then
len (Upper_Seq (C,n)) >= 2
by XXREAL_0:2;
then
2 in Seg (len (Upper_Seq (C,n)))
by FINSEQ_1:1;
then A2:
2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))
by JORDAN1E:8;
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. 1 = W-min (L~ (Cage (C,n)))
by FINSEQ_5:53;
then A3:
W-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by FINSEQ_6:42;
(Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n)))
by JORDAN9:32;
then
(W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n))
by SPRECT_2:76;
then A4:
((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))) + 1 <= len (Cage (C,n))
by NAT_1:13;
( W-max (L~ (Cage (C,n))) in L~ (Cage (C,n)) & (N-min (L~ (Cage (C,n)))) `2 = N-bound (L~ (Cage (C,n))) )
by EUCLID:52, SPRECT_1:13;
then
(W-max (L~ (Cage (C,n)))) `2 <= (N-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:24;
then
N-min (L~ (Cage (C,n))) <> W-min (L~ (Cage (C,n)))
by SPRECT_2:57;
then A5:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} = 2
by CARD_2:57;
A6:
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
then A7:
1 <= (W-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by FINSEQ_4:21;
((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) /. (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) =
(Cage (C,n)) /. (len (Cage (C,n)))
by A6, FINSEQ_5:54
.=
(Cage (C,n)) /. 1
by FINSEQ_6:def 1
.=
N-min (L~ (Cage (C,n)))
by JORDAN9:32
;
then A8:
N-min (L~ (Cage (C,n))) in rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by FINSEQ_6:168;
{(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by A8, A3, TARSKI:def 2;
then A9:
card {(N-min (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n))))} c= card (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by CARD_1:11;
card (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) c= card (dom ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by CARD_2:61;
then
card (rng ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))) c= len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n)))))
by CARD_1:62;
then
Segm 2 c= Segm (len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))))
by A5, A9;
then A10:
len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 2
by NAT_1:39;
then A11:
len ((Cage (C,n)) :- (W-min (L~ (Cage (C,n))))) >= 1
by XXREAL_0:2;
A12: (Upper_Seq (C,n)) /. 1 =
((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. 1
by JORDAN1E:def 1
.=
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1
by A1, FINSEQ_5:44
.=
(Cage (C,n)) /. ((1 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))
by A6, A11, FINSEQ_6:174
.=
(Cage (C,n)) /. (0 + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))
by XREAL_1:232
;
(Upper_Seq (C,n)) /. 2 =
((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. 2
by JORDAN1E:def 1
.=
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 2
by A1, A2, FINSEQ_5:43
.=
(Cage (C,n)) /. ((2 -' 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))
by A6, A10, FINSEQ_6:174
.=
(Cage (C,n)) /. ((2 - 1) + ((W-min (L~ (Cage (C,n)))) .. (Cage (C,n))))
by XREAL_0:def 2
;
hence
((Upper_Seq (C,n)) /. 2) `1 = W-bound (L~ (Cage (C,n)))
by A7, A4, A12, JORDAN1E:22, JORDAN1F:5; verum