let C be Simple_closed_curve; :: thesis:
let n, m be Element of NAT ; :: thesis:
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; :: thesis:
set i1 = X-SpanStart C,m;
set G1 = Gauge C,m;
set YI = Y-InitStart C;
set AI = ApproxIndex C;
A3: m is_sufficiently_large_for C by A1, A2, Th29;
then A4: ApproxIndex C <= m by JORDAN11:def 1;
set i = X-SpanStart C,n;
set G = Gauge C,n;
A5: 1 <= (X-SpanStart C,m) -' 1 by JORDAN1H:59;
set j1 = Y-SpanStart C,m;
set f1 = Span C,m;
Y-SpanStart C,m <= ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A3, JORDAN11:5;
then A6: (cell (Gauge C,m),((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) \ (L~ (Span C,m)) c= BDD (L~ (Span C,m)) by A1, A2, Th29, Th31;
A7: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
then (X-SpanStart C,n) + 1 <= len (Gauge C,n) by NAT_1:13;
then A8: X-SpanStart C,n <= (len (Gauge C,n)) - 1 by XREAL_1:21;
set XSAI = X-SpanStart C,(ApproxIndex C);
set p2 = (Gauge C,(ApproxIndex C)) * (X-SpanStart C,(ApproxIndex C)),(Y-InitStart C);
A9: 1 < X-SpanStart C,(ApproxIndex C) by JORDAN1H:58, XXREAL_0:2;
A10: (Y-InitStart C) + 1 < width (Gauge C,(ApproxIndex C)) by JORDAN11:3;
then A11: Y-InitStart C < width (Gauge C,(ApproxIndex C)) by NAT_1:13;
set j4 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A12: X-SpanStart C,m < len (Gauge C,m) by JORDAN1H:58;
set j = Y-SpanStart C,n;
set f = Span C,n;
Y-SpanStart C,n <= ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A1, JORDAN11:5;
then A13: (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) \ (L~ (Span C,n)) c= BDD (L~ (Span C,n)) by A1, Th31;
A14: Int (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) c= cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) by TOPS_1:44;
A15: 2 < X-SpanStart C,n by JORDAN1H:58;
then A16: ((X-SpanStart C,n) -' 1) + 1 = X-SpanStart C,n by XREAL_1:237, XXREAL_0:2;
then A17: (X-SpanStart C,n) -' 1 >= 1 + 1 by A15, NAT_1:13;
set j3 = ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2;
A18: X-SpanStart C,n < len (Gauge C,n) by JORDAN1H:58;
A19: Y-InitStart C > 1 by JORDAN11:2;
then Y-InitStart C >= (1 + 1) + 0 by NAT_1:13;
then A20: (Y-InitStart C) - 2 >= 0 by XREAL_1:21;
then A21: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 = ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by XREAL_0:def 2;
A22: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 = ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) - 2)) + 2 by A20, XREAL_0:def 2;
then A23: 1 < ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A4, A11, A19, JORDAN1A:53;
set p3 = (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)));
A24: (X-SpanStart C,m) -' 1 < len (Gauge C,m) by JORDAN1H:59;
A25: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge C,m) by A4, A11, A19, A22, JORDAN1A:53;
then A26: (((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= width (Gauge C,m) by NAT_1:13;
2 < X-SpanStart C,m by JORDAN1H:58;
then A27: ((X-SpanStart C,m) -' 1) + 1 = X-SpanStart C,m by XREAL_1:237, XXREAL_0:2;
then A28: (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in Int (cell (Gauge C,m),((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by A12, A23, A5, A26, GOBOARD6:34;
then A29: ((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 < ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `2 by A12, A23, A27, A5, A26, Th4;
A30: ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `2 < ((Gauge C,m) * ((X-SpanStart C,m) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A12, A23, A27, A5, A26, A28, Th4;
A31: ((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `1 < ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `1 by A12, A23, A27, A5, A26, A28, Th4;
A32: 1 < X-SpanStart C,m by JORDAN1H:58, XXREAL_0:2;
then A33: ((Gauge C,m) * (X-SpanStart C,m),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 = ((Gauge C,m) * 1,(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 by A12, A23, A25, GOBOARD5:2
.= ((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 by A23, A25, A5, A24, GOBOARD5:2 ;
A34: (((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 >= 1 by NAT_1:11;
then A35: ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 = ((Gauge C,m) * 1,((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A12, A32, A26, GOBOARD5:2
.= ((Gauge C,m) * ((X-SpanStart C,m) -' 1),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A5, A24, A26, A34, GOBOARD5:2 ;
A36: 1 <= (X-SpanStart C,n) -' 1 by JORDAN1H:59;
A37: ApproxIndex C <= n by A1, JORDAN11:def 1;
then A38: 1 < ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 by A11, A19, A21, JORDAN1A:53;
(Y-InitStart C) + 1 < len (Gauge C,(ApproxIndex C)) by A10, JORDAN8:def 1;
then (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 < len (Gauge C,n) by A37, A21, Th32, JORDAN11:2;
then ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) + 1 <= len (Gauge C,n) by NAT_1:13;
then A39: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= (len (Gauge C,n)) - 1 by XREAL_1:21;
A40: (X-SpanStart C,n) -' 1 < len (Gauge C,n) by JORDAN1H:59;
then ((X-SpanStart C,n) -' 1) + 1 <= len (Gauge C,n) by NAT_1:13;
then A41: (X-SpanStart C,n) -' 1 <= (len (Gauge C,n)) - 1 by XREAL_1:21;
A42: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge C,n) by A37, A11, A19, A21, JORDAN1A:53;
then A43: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= width (Gauge C,n) by NAT_1:13;
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < len (Gauge C,n) by A42, JORDAN8:def 1;
then (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 <= len (Gauge C,n) by NAT_1:13;
then A44: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 <= (len (Gauge C,n)) - 1 by XREAL_1:21;
A45: X-SpanStart C,(ApproxIndex C) < len (Gauge C,(ApproxIndex C)) by JORDAN1H:58;
X-SpanStart C,m = ((2 |^ (m -' (ApproxIndex C))) * ((X-SpanStart C,(ApproxIndex C)) - 2)) + 2 by A1, A2, Th29, JORDAN11:4;
then A46: (Gauge C,(ApproxIndex C)) * (X-SpanStart C,(ApproxIndex C)),(Y-InitStart C) = (Gauge C,m) * (X-SpanStart C,m),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) by A4, A9, A45, A11, A19, A22, JORDAN1A:54;
A47: X-SpanStart C,n = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart C,(ApproxIndex C)) - 2)) + 2 by A1, JORDAN11:4;
then A48: (Gauge C,(ApproxIndex C)) * (X-SpanStart C,(ApproxIndex C)),(Y-InitStart C) = (Gauge C,n) * (X-SpanStart C,n),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) by A37, A9, A45, A11, A19, A21, JORDAN1A:54;
A49: 1 < X-SpanStart C,n by JORDAN1H:58, XXREAL_0:2;
then ((Gauge C,n) * (X-SpanStart C,n),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 = ((Gauge C,n) * 1,(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 by A18, A38, A42, GOBOARD5:2
.= ((Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 by A38, A42, A36, A40, GOBOARD5:2 ;
then A50: ((Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `2 < ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `2 by A47, A37, A9, A45, A11, A19, A21, A46, A29, A33, JORDAN1A:54;
((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `1 < ((Gauge C,m) * (X-SpanStart C,m),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `1 by A12, A23, A27, A5, A26, A28, Th4;
then A51: ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `1 < ((Gauge C,n) * (X-SpanStart C,n),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `1 by A47, A37, A9, A45, A11, A19, A21, A46, JORDAN1A:54;
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 >= 1 + 1 by A38, NAT_1:13;
then ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,m)) - 1 & 2 <= d & d <= (len (Gauge C,m)) - 1 & [c,d] in Indices (Gauge C,m) & (Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) = (Gauge C,m) * c,d & c = 2 + ((2 |^ (m -' n)) * (((X-SpanStart C,n) -' 1) -' 2)) & d = 2 + ((2 |^ (m -' n)) * ((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) -' 2)) ) by A2, A17, A41, A44, GOBRD14:18;
then (Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) in { ((Gauge C,m) * ii,jj) where ii, jj is Element of NAT : [ii,jj] in Indices (Gauge C,m) } ;
then (Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) in Values (Gauge C,m) by GOBRD13:7;
then ((Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `1 <= ((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `1 by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13:15;
then A52: ((Gauge C,n) * ((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) `1 < ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `1 by A31, XXREAL_0:2;
(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 > 1 + 1 by A38, XREAL_1:8;
then ex c, d being Element of NAT st
( 2 <= c & c <= (len (Gauge C,m)) - 1 & 2 <= d & d <= (len (Gauge C,m)) - 1 & [c,d] in Indices (Gauge C,m) & (Gauge C,n) * (X-SpanStart C,n),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) = (Gauge C,m) * c,d & c = 2 + ((2 |^ (m -' n)) * ((X-SpanStart C,n) -' 2)) & d = 2 + ((2 |^ (m -' n)) * (((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) -' 2)) ) by A2, A15, A8, A39, GOBRD14:18;
then (Gauge C,n) * (X-SpanStart C,n),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) in { ((Gauge C,m) * ii,jj) where ii, jj is Element of NAT : [ii,jj] in Indices (Gauge C,m) } ;
then (Gauge C,n) * (X-SpanStart C,n),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1) in Values (Gauge C,m) by GOBRD13:7;
then A53: ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 <= ((Gauge C,n) * (X-SpanStart C,n),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A48, A46, A49, A18, A38, A42, A12, A32, A23, A25, GOBRD13:16;
A54: (((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1 >= 1 by NAT_1:11;
then ((Gauge C,n) * (X-SpanStart C,n),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 = ((Gauge C,n) * 1,((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A49, A18, A43, GOBOARD5:2
.= ((Gauge C,n) * ((X-SpanStart C,n) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A36, A40, A43, A54, GOBOARD5:2 ;
then ((1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)))) `2 < ((Gauge C,n) * ((X-SpanStart C,n) -' 1),((((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1)) `2 by A30, A35, A53, XXREAL_0:2;
then A55: (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in Int (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) by A7, A38, A16, A36, A52, A51, A43, A50, Th4;
Span C,n is_sequence_on Gauge C,n by A1, JORDAN13:def 1;
then Int (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) misses L~ (Span C,n) by A42, A40, JORDAN9:16;
then not (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in L~ (Span C,n) by A55, XBOOLE_0:3;
then (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in (cell (Gauge C,n),((X-SpanStart C,n) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) \ (L~ (Span C,n)) by A55, A14, XBOOLE_0:def 5;
then (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in BDD (L~ (Span C,n)) by A13;
then A56: (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in RightComp (Span C,n) by GOBRD14:47;
Span C,m is_sequence_on Gauge C,m by A3, JORDAN13:def 1;
then Int (cell (Gauge C,m),((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) misses L~ (Span C,m) by A25, A24, JORDAN9:16;
then A57: not (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in L~ (Span C,m) by A28, XBOOLE_0:3;
Int (cell (Gauge C,m),((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) c= cell (Gauge C,m),((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) by TOPS_1:44;
then (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in (cell (Gauge C,m),((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) \ (L~ (Span C,m)) by A28, A57, XBOOLE_0:def 5;
then (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in BDD (L~ (Span C,m)) by A6;
then (1 / 2) * (((Gauge C,m) * ((X-SpanStart C,m) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2)) + ((Gauge C,m) * (X-SpanStart C,m),((((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2) + 1))) in RightComp (Span C,m) by GOBRD14:47;
hence RightComp (Span C,n) meets RightComp (Span C,m) by A56, XBOOLE_0:3; :: thesis: