let m, n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-bound (L~ (Cage (C,n)))) + (S-bound (L~ (Cage (C,n)))) = (N-bound (L~ (Cage (C,m)))) + (S-bound (L~ (Cage (C,m))))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (N-bound (L~ (Cage (C,n)))) + (S-bound (L~ (Cage (C,n)))) = (N-bound (L~ (Cage (C,m)))) + (S-bound (L~ (Cage (C,m))))
thus (N-bound (L~ (Cage (C,n)))) + (S-bound (L~ (Cage (C,n)))) = ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) + (S-bound (L~ (Cage (C,n)))) by JORDAN10:6
.= ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))) + ((S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ n))) by Th63
.= ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ m))) + ((S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ m)))
.= ((N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ m))) + (S-bound (L~ (Cage (C,m)))) by Th63
.= (N-bound (L~ (Cage (C,m)))) + (S-bound (L~ (Cage (C,m)))) by JORDAN10:6 ; :: thesis: verum