let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) & W-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) & W-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
set p = W-min (L~ (Cage C,n));
A1: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A2: E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_6:96, SPRECT_2:47;
Upper_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) -: (E-max (L~ (Cage C,n))) by JORDAN1E:def 1;
then (Upper_Seq C,n) /. 1 = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by A2, FINSEQ_5:47;
then (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n)) by A1, FINSEQ_6:98;
hence A3: W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) by FINSEQ_6:46; :: thesis: W-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n)
len (Upper_Seq C,n) >= 2 by TOPREAL1:def 10;
then rng (Upper_Seq C,n) c= L~ (Upper_Seq C,n) by SPPOL_2:18;
hence W-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n) by A3; :: thesis: verum