let n be 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 FINSEQ_6:168; :: thesis: W-min (L~ (Cage (C,n))) in L~ (Lower_Seq (C,n))
len (Lower_Seq (C,n)) >= 2 by TOPREAL1:def 8;
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