let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage C,n)) = (S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: S-bound (L~ (Cage C,n)) = (S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ n))
set a = N-bound C;
set s = S-bound C;
set w = W-bound C;
set e = E-bound C;
set f = Cage C,n;
set G = Gauge C,n;
consider p, q being Element of NAT such that
A1: ( 1 <= p & p < len (Cage C,n) & 1 <= q & q <= len (Gauge C,n) ) and
A2: (Cage C,n) /. p = (Gauge C,n) * q,1 by Th77;
A3: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
(Cage C,n) /. p in S-most (L~ (Cage C,n)) by A1, A2, Th81;
then A4: ((Cage C,n) /. p) `2 = (S-min (L~ (Cage C,n))) `2 by PSCOMP_1:118;
4 <= len (Gauge C,n) by JORDAN8:13;
then 1 <= len (Gauge C,n) by XXREAL_0:2;
then A5: [q,1] in Indices (Gauge C,n) by A1, A3, MATRIX_1:37;
thus S-bound (L~ (Cage C,n)) = (S-min (L~ (Cage C,n))) `2 by EUCLID:56
.= |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (q - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| `2 by A2, A4, A5, JORDAN8:def 1
.= (S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ n)) by EUCLID:56 ; :: thesis: verum