let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n))
let n be Element of NAT ; :: thesis: L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n))
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then 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;
then L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) by SPPOL_2:25;
hence L~ (Cage C,n) = (L~ (Upper_Seq C,n)) \/ (L~ (Lower_Seq C,n)) by REVROT_1:33; :: thesis: verum