let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Nat holds (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1

let n be 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 Th8

.= ((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 Th9

.= ((((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 FINSEQ_6:179 ; :: thesis: verum

let n be 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 Th8

.= ((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 Th9

.= ((((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 FINSEQ_6:179 ; :: thesis: verum