let C be Simple_closed_curve; :: thesis: for n, m being Nat st n is_sufficiently_large_for C & n <= m holds
RightComp (Span (C,n)) meets RightComp (Span (C,m))
let n, m be Nat; :: thesis: ( n is_sufficiently_large_for C & n <= m implies RightComp (Span (C,n)) meets RightComp (Span (C,m)) )
assume that
A1: n is_sufficiently_large_for C and
A2: n <= m ; :: thesis: RightComp (Span (C,n)) meets RightComp (Span (C,m))
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, Th28;
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:50;
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, Th28, Th30;
A7: X-SpanStart (C,n) < len (Gauge (C,n)) by JORDAN1H:49;
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:19;
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:49, 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:49;
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, Th30;
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:16;
A15: 2 < X-SpanStart (C,n) by JORDAN1H:49;
then A16: ((X-SpanStart (C,n)) -' 1) + 1 = X-SpanStart (C,n) by XREAL_1:235, 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:49;
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:19;
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:32;
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:50;
A25: ((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge (C,m)) by A4, A11, A19, A22, JORDAN1A:32;
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:49;
then A27: ((X-SpanStart (C,m)) -' 1) + 1 = X-SpanStart (C,m) by XREAL_1:235, 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:31;
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:49, 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:1
.= ((Gauge (C,m)) * (((X-SpanStart (C,m)) -' 1),(((2 |^ (m -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A23, A25, A5, A24, GOBOARD5:1 ;
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:1
.= ((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:1 ;
A36: 1 <= (X-SpanStart (C,n)) -' 1 by JORDAN1H:50;
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:32;
(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, Th31, 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:19;
A40: (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) by JORDAN1H:50;
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:19;
A42: ((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 < width (Gauge (C,n)) by A37, A11, A19, A21, JORDAN1A:32;
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:19;
A45: X-SpanStart (C,(ApproxIndex C)) < len (Gauge (C,(ApproxIndex C))) by JORDAN1H:49;
X-SpanStart (C,m) = ((2 |^ (m -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by A1, A2, Th28, 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:33;
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:33;
A49: 1 < X-SpanStart (C,n) by JORDAN1H:49, 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:1
.= ((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2))) `2 by A38, A42, A36, A40, GOBOARD5:1 ;
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:33;
((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:33;
((2 |^ (n -' (ApproxIndex C))) * ((Y-InitStart C) -' 2)) + 2 >= 1 + 1 by A38, NAT_1:13;
then ex c, d being 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:8;
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 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 MATRIX_0:39;
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:14;
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:6;
then ex c, d being 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:8;
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 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 MATRIX_0:39;
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:15;
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:1
.= ((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:1 ;
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:14;
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:37;
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:14;
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:16;
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:37;
hence RightComp (Span (C,n)) meets RightComp (Span (C,m)) by A56, XBOOLE_0:3; :: thesis: verum