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