let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being 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 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:46;

then A1: 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 rng (Upper_Seq (C,n)) c= rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:48;

hence rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) by FINSEQ_6:90, SPRECT_2:43; :: 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:55;

hence rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) by FINSEQ_6:90, SPRECT_2:43; :: thesis: verum

( rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) & rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) )

let n be 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:46;

then A1: 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 rng (Upper_Seq (C,n)) c= rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:48;

hence rng (Upper_Seq (C,n)) c= rng (Cage (C,n)) by FINSEQ_6:90, SPRECT_2:43; :: 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:55;

hence rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) by FINSEQ_6:90, SPRECT_2:43; :: thesis: verum