set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));

A25: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;

W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

then A26: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A25, FINSEQ_6:92;

then (W-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A25, SPRECT_5:23;

then (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A25, A26, SPRECT_5:22, XXREAL_0:2;

then (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A25, A26, SPRECT_5:24, XXREAL_0:2;

then A27: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A25, A26, SPRECT_5:25, XXREAL_0:2;

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A28: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

A29: len (Lower_Seq (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))) in rng (Cage (C,n)) by SPRECT_2:46;

then A46: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

hence Lower_Seq (C,n) is special by SPPOL_2:39; :: thesis: ( Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )

thus Lower_Seq (C,n) is unfolded by A46, SPPOL_2:27; :: thesis: Lower_Seq (C,n) is s.n.c.

let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) )

assume A47: i + 1 < j ; :: thesis: LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j)

i + 1 >= 1 by NAT_1:11;

then j = (j -' 1) + 1 by A47, XREAL_1:235, XXREAL_0:2;

then A48: LSeg ((Lower_Seq (C,n)),j) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A46, SPPOL_2:10;

A25: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;

W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;

then A26: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A25, FINSEQ_6:92;

then (W-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A25, SPRECT_5:23;

then (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A25, A26, SPRECT_5:22, XXREAL_0:2;

then (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A25, A26, SPRECT_5:24, XXREAL_0:2;

then A27: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A25, A26, SPRECT_5:25, XXREAL_0:2;

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A28: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

A29: len (Lower_Seq (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;

now :: thesis: for i1, j1 being object st i1 in dom (Lower_Seq (C,n)) & j1 in dom (Lower_Seq (C,n)) & (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 holds

not i1 <> j1

hence
Lower_Seq (C,n) is one-to-one
by FUNCT_1:def 4; :: thesis: ( Lower_Seq (C,n) is special & Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )not i1 <> j1

let i1, j1 be object ; :: thesis: ( i1 in dom (Lower_Seq (C,n)) & j1 in dom (Lower_Seq (C,n)) & (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 implies not i1 <> j1 )

assume that

A30: i1 in dom (Lower_Seq (C,n)) and

A31: j1 in dom (Lower_Seq (C,n)) and

A32: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 and

A33: i1 <> j1 ; :: thesis: contradiction

reconsider i2 = i1, j2 = j1 as Nat by A30, A31;

A34: i2 in Seg (len (Lower_Seq (C,n))) by A30, FINSEQ_1:def 3;

then i2 >= 1 by FINSEQ_1:1;

then A35: i2 = (i2 -' 1) + 1 by XREAL_1:235;

A36: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) /. i2 by A30, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A28, A30, A35, FINSEQ_5:52 ;

A37: j2 in Seg (len (Lower_Seq (C,n))) by A31, FINSEQ_1:def 3;

then j2 >= 1 by FINSEQ_1:1;

then A38: j2 = (j2 -' 1) + 1 by XREAL_1:235;

A39: (Lower_Seq (C,n)) . j1 = (Lower_Seq (C,n)) /. j2 by A31, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A28, A31, A38, FINSEQ_5:52 ;

0 + 1 <= i2 by A34, FINSEQ_1:1;

then A40: i2 - 1 >= 0 by XREAL_1:19;

i2 <= ((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 A29, A34, FINSEQ_1:1;

then i2 - 1 <= (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))))))) by XREAL_1:20;

then (i2 - 1) + ((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)))))) by XREAL_1:19;

then A41: (i2 -' 1) + ((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)))))) by A40, XREAL_0:def 2;

0 + 1 <= j2 by A37, FINSEQ_1:1;

then A42: j2 - 1 >= 0 by XREAL_1:19;

j2 <= ((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 A29, A37, FINSEQ_1:1;

then j2 - 1 <= (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))))))) by XREAL_1:20;

then (j2 - 1) + ((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)))))) by XREAL_1:19;

then A43: (j2 -' 1) + ((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)))))) by A42, XREAL_0:def 2;

(j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (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)))))) by NAT_1:11;

then A44: 1 < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A27, XXREAL_0:2;

(i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (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)))))) by NAT_1:11;

then A45: 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A27, XXREAL_0:2;

end;assume that

A30: i1 in dom (Lower_Seq (C,n)) and

A31: j1 in dom (Lower_Seq (C,n)) and

A32: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 and

A33: i1 <> j1 ; :: thesis: contradiction

reconsider i2 = i1, j2 = j1 as Nat by A30, A31;

A34: i2 in Seg (len (Lower_Seq (C,n))) by A30, FINSEQ_1:def 3;

then i2 >= 1 by FINSEQ_1:1;

then A35: i2 = (i2 -' 1) + 1 by XREAL_1:235;

A36: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) /. i2 by A30, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A28, A30, A35, FINSEQ_5:52 ;

A37: j2 in Seg (len (Lower_Seq (C,n))) by A31, FINSEQ_1:def 3;

then j2 >= 1 by FINSEQ_1:1;

then A38: j2 = (j2 -' 1) + 1 by XREAL_1:235;

A39: (Lower_Seq (C,n)) . j1 = (Lower_Seq (C,n)) /. j2 by A31, PARTFUN1:def 6

.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A28, A31, A38, FINSEQ_5:52 ;

0 + 1 <= i2 by A34, FINSEQ_1:1;

then A40: i2 - 1 >= 0 by XREAL_1:19;

i2 <= ((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 A29, A34, FINSEQ_1:1;

then i2 - 1 <= (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))))))) by XREAL_1:20;

then (i2 - 1) + ((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)))))) by XREAL_1:19;

then A41: (i2 -' 1) + ((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)))))) by A40, XREAL_0:def 2;

0 + 1 <= j2 by A37, FINSEQ_1:1;

then A42: j2 - 1 >= 0 by XREAL_1:19;

j2 <= ((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 A29, A37, FINSEQ_1:1;

then j2 - 1 <= (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))))))) by XREAL_1:20;

then (j2 - 1) + ((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)))))) by XREAL_1:19;

then A43: (j2 -' 1) + ((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)))))) by A42, XREAL_0:def 2;

(j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (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)))))) by NAT_1:11;

then A44: 1 < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A27, XXREAL_0:2;

(i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (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)))))) by NAT_1:11;

then A45: 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A27, XXREAL_0:2;

per cases
( i2 < j2 or j2 < i2 )
by A33, XXREAL_0:1;

end;

suppose
i2 < j2
; :: thesis: contradiction

then
i2 - 1 < j2 - 1
by XREAL_1:9;

then i2 - 1 < j2 -' 1 by XREAL_0:def 2;

then i2 -' 1 < j2 -' 1 by A40, XREAL_0:def 2;

then (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;

hence contradiction by A32, A36, A39, A43, A45, GOBOARD7:37; :: thesis: verum

end;then i2 - 1 < j2 -' 1 by XREAL_0:def 2;

then i2 -' 1 < j2 -' 1 by A40, XREAL_0:def 2;

then (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;

hence contradiction by A32, A36, A39, A43, A45, GOBOARD7:37; :: thesis: verum

suppose
j2 < i2
; :: thesis: contradiction

then
j2 - 1 < i2 - 1
by XREAL_1:9;

then j2 - 1 < i2 -' 1 by XREAL_0:def 2;

then j2 -' 1 < i2 -' 1 by A42, XREAL_0:def 2;

then (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;

hence contradiction by A32, A36, A39, A41, A44, GOBOARD7:37; :: thesis: verum

end;then j2 - 1 < i2 -' 1 by XREAL_0:def 2;

then j2 -' 1 < i2 -' 1 by A42, XREAL_0:def 2;

then (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;

hence contradiction by A32, A36, A39, A41, A44, GOBOARD7:37; :: thesis: verum

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A46: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

hence Lower_Seq (C,n) is special by SPPOL_2:39; :: thesis: ( Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )

thus Lower_Seq (C,n) is unfolded by A46, SPPOL_2:27; :: thesis: Lower_Seq (C,n) is s.n.c.

let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) )

assume A47: i + 1 < j ; :: thesis: LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j)

i + 1 >= 1 by NAT_1:11;

then j = (j -' 1) + 1 by A47, XREAL_1:235, XXREAL_0:2;

then A48: LSeg ((Lower_Seq (C,n)),j) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A46, SPPOL_2:10;

now :: thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} end;

hence
LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j)
; :: thesis: verumper cases
( i > 0 or i = 0 )
;

end;

suppose
i > 0
; :: thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}

then A49:
i >= 0 + 1
by NAT_1:13;

then i = (i -' 1) + 1 by XREAL_1:235;

then A50: LSeg ((Lower_Seq (C,n)),i) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A28, SPPOL_2:10;

(i + 1) - 1 < j - 1 by A47, XREAL_1:9;

then A51: (i - 1) + 1 < j -' 1 by XREAL_0:def 2;

i - 1 >= 0 by A49, XREAL_1:19;

then (i -' 1) + 1 < j -' 1 by A51, XREAL_0:def 2;

then ((i -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;

then A52: ((i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ;

A53: (i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) > 0 + 1 by A27, XREAL_1:8;

end;then i = (i -' 1) + 1 by XREAL_1:235;

then A50: LSeg ((Lower_Seq (C,n)),i) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A28, SPPOL_2:10;

(i + 1) - 1 < j - 1 by A47, XREAL_1:9;

then A51: (i - 1) + 1 < j -' 1 by XREAL_0:def 2;

i - 1 >= 0 by A49, XREAL_1:19;

then (i -' 1) + 1 < j -' 1 by A51, XREAL_0:def 2;

then ((i -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;

then A52: ((i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ;

A53: (i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) > 0 + 1 by A27, XREAL_1:8;

now :: thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} end;

hence
(LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}
; :: thesis: verumper cases
( ((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) or ((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 > len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) )
;

end;

suppose
((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}

then
(j -' 1) + ((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))))))
by NAT_1:13;

then LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) by A48, A50, A52, A53, GOBOARD5:def 4;

hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; :: thesis: verum

end;then LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) by A48, A50, A52, A53, GOBOARD5:def 4;

hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; :: thesis: verum

suppose
((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 > len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
; :: thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}

then
LSeg ((Lower_Seq (C,n)),j) = {}
by A48, TOPREAL1:def 3;

hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; :: thesis: verum

end;hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; :: thesis: verum