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

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