let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
let n be 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:46;
then 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;
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:24;
hence L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by REVROT_1:33; :: thesis: verum