let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds
( rng (Upper_Seq C,n) c= rng (Cage C,n) & rng (Lower_Seq C,n) c= rng (Cage C,n) )
let n be Element of NAT ; :: thesis: ( rng (Upper_Seq C,n) c= rng (Cage C,n) & rng (Lower_Seq C,n) c= rng (Cage C,n) )
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A1: 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 rng (Upper_Seq C,n) c= rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_5:51;
hence rng (Upper_Seq C,n) c= rng (Cage C,n) by FINSEQ_6:96, SPRECT_2:47; :: thesis: rng (Lower_Seq C,n) c= rng (Cage C,n)
Lower_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n))) by JORDAN1E:def 2;
then rng (Lower_Seq C,n) c= rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A1, FINSEQ_5:58;
hence rng (Lower_Seq C,n) c= rng (Cage C,n) by FINSEQ_6:96, SPRECT_2:47; :: thesis: verum