let C be compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat holds L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))
let n be Nat; 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; verum