let C be 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)) ^' (Lower_Seq (C,n)))
let n be Nat; :: thesis: L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))
Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n)) by Th11;
hence L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) by REVROT_1:33; :: thesis: verum