let n be Element of 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:47;
then A1: W-min (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:50;
len (Lower_Seq C,n) >= 3 by JORDAN1E:19;
then len (Lower_Seq C,n) >= 2 by XXREAL_0:2;
then 2 <= (W-min (L~ (Cage C,n))) .. (Lower_Seq C,n) by Th38;
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 Th26;
then 2 <= (W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) by A1, FINSEQ_6:77;
then A2: 2 in Seg ((W-min (L~ (Cage C,n))) .. (Rotate (Cage C,n),(E-max (L~ (Cage C,n))))) by FINSEQ_1:3;
((Cage C,n) :- (E-max (L~ (Cage C,n)))) /. 1 = E-max (L~ (Cage C,n)) by FINSEQ_5:56;
then A3: E-max (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by FINSEQ_6:46;
( 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:56, SPRECT_1:13;
then (N-max (L~ (Cage C,n))) `1 <= (E-max (L~ (Cage C,n))) `1 by PSCOMP_1:71;
then N-min (L~ (Cage C,n)) <> E-max (L~ (Cage C,n)) by SPRECT_2:55;
then A4: card {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} = 2 by CARD_2:76;
A5: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (E-min (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:75;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A5, SPRECT_2:76, 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:77, 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:78, XXREAL_0:2;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by A5, SPRECT_2:80, 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:50;
then A8: 1 <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by FINSEQ_4:31;
((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:57
.= (Cage C,n) /. 1 by FINSEQ_6:def 1
.= N-min (L~ (Cage C,n)) by JORDAN9:34 ;
then A9: N-min (L~ (Cage C,n)) in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by REVROT_1:3;
{(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} c= rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} or x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) )
assume x in {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))} ; :: thesis: x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n))))
hence x in rng ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by A9, A3, TARSKI:def 2; :: thesis: verum

end;

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:27;
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:80;
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:104;
then 2 c= len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) by A4, A10, XBOOLE_1:1;
then A11: len ((Cage C,n) :- (E-max (L~ (Cage C,n)))) >= 2 by NAT_1:40;
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 Th26
.= (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 1 by A1, FINSEQ_5:47
.= (Cage C,n) /. ((1 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) by A7, A12, REVROT_1:9
.= (Cage C,n) /. (0 + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) by XREAL_1:234 ;
(Lower_Seq C,n) /. 2 = ((Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n)))) /. 2 by Th26
.= (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) /. 2 by A1, A2, FINSEQ_5:46
.= (Cage C,n) /. ((2 -' 1) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) by A7, A11, REVROT_1:9
.= (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:24, JORDAN1F:6; :: thesis: verum