let n be Nat; 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); ( 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; 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; verum