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 (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:43;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A2: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
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:44;
then (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92;
hence A3: W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by FINSEQ_6:42; :: thesis: W-min (L~ (Cage (C,n))) in L~ (Upper_Seq (C,n))
len (Upper_Seq (C,n)) >= 2 by TOPREAL1:def 8;
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