let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( N-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) & N-max (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n)) )
set x = N-max (L~ (Cage (C,n)));
set p = W-min (L~ (Cage (C,n)));
set f = Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))));
A1: rng (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) = rng (Cage (C,n)) by FINSEQ_6:90, SPRECT_2:46;
A2: N-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:40;
A3: (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n))) by JORDAN1F:6;
A4: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) by REVROT_1:33;
W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A5: 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;
A6: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) -: (W-min (L~ (Cage (C,n)))) by JORDAN1G:18;
then A7: (Lower_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) /. 1 by A5, FINSEQ_5:44;
then A8: (W-min (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) < (W-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) by A4, JORDAN1F:6, SPRECT_5:42;
A9: (W-max (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) <= (N-min (L~ (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(E-max (L~ (Cage (C,n)))))) by A7, A4, JORDAN1F:6, SPRECT_5:43;