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 (Lower_Seq C,n) & W-min (L~ (Cage C,n)) in L~ (Lower_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 (Lower_Seq C,n) & W-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n) )
set p = W-min (L~ (Cage C,n));
(Lower_Seq C,n) /. (len (Lower_Seq C,n)) = W-min (L~ (Cage C,n)) by JORDAN1F:8;
hence A1: W-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) by REVROT_1:3; :: thesis: W-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n)
len (Lower_Seq C,n) >= 2 by TOPREAL1:def 10;
then rng (Lower_Seq C,n) c= L~ (Lower_Seq C,n) by SPPOL_2:18;
hence W-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n) by A1; :: thesis: verum