let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds (len (Upper_Seq C,n)) + (len (Lower_Seq C,n)) = (len (Cage C,n)) + 1
let n be Element of NAT ; :: thesis: (len (Upper_Seq C,n)) + (len (Lower_Seq C,n)) = (len (Cage C,n)) + 1
thus (len (Upper_Seq C,n)) + (len (Lower_Seq C,n)) = ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) + (len (Lower_Seq C,n)) by Th12
.= ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) + (((len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) - ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1) by Th13
.= ((((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) + (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) - ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))))) + 1
.= (len (Cage C,n)) + 1 by REVROT_1:14 ; :: thesis: verum