let C be 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) ^' (Lower_Seq C,n))
let n be Element of 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 Th15;
hence L~ (Cage C,n) = L~ ((Upper_Seq C,n) ^' (Lower_Seq C,n)) by REVROT_1:33; :: thesis: verum