let n be Nat; :: thesis: 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); :: thesis: ((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; :: thesis: verum

let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ((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; :: thesis: verum