set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A26: 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:47;
then A27: (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 A26, FINSEQ_6:98;
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 A26, SPRECT_5:24;
then (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A26, A27, SPRECT_5:23, XXREAL_0:2;
then (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A26, A27, SPRECT_5:25, XXREAL_0:2;
then A28: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A26, A27, SPRECT_5:26, XXREAL_0:2;
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:50;
then A29: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:96, SPRECT_2:47;
A30: 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 Th13;

now

let i1, j1 be set ; :: 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
A31: i1 in dom (Lower_Seq (C,n)) and
A32: j1 in dom (Lower_Seq (C,n)) and
A33: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 and
A34: i1 <> j1 ; :: thesis: contradiction
reconsider i2 = i1, j2 = j1 as Element of NAT by A31, A32;
A35: i2 in Seg (len (Lower_Seq (C,n))) by A31, FINSEQ_1:def 3;
then i2 >= 1 by FINSEQ_1:3;
then A36: i2 = (i2 -' 1) + 1 by XREAL_1:237;
A37: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) /. i2 by A31, PARTFUN1:def 8
.= (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 A29, A31, A36, FINSEQ_5:55 ;
A38: j2 in Seg (len (Lower_Seq (C,n))) by A32, FINSEQ_1:def 3;
then j2 >= 1 by FINSEQ_1:3;
then A39: j2 = (j2 -' 1) + 1 by XREAL_1:237;
A40: (Lower_Seq (C,n)) . j1 = (Lower_Seq (C,n)) /. j2 by A32, PARTFUN1:def 8
.= (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 A29, A32, A39, FINSEQ_5:55 ;
0 + 1 <= i2 by A35, FINSEQ_1:3;
then A41: i2 - 1 >= 0 by XREAL_1:21;
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 A30, A35, FINSEQ_1:3;
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:22;
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:21;
then A42: (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 A41, XREAL_0:def 2;
0 + 1 <= j2 by A38, FINSEQ_1:3;
then A43: j2 - 1 >= 0 by XREAL_1:21;
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 A30, A38, FINSEQ_1:3;
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:22;
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:21;
then A44: (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 A43, 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 A45: 1 < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A28, 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 A46: 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A28, XXREAL_0:2;

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

suppose i2 < j2 ; :: thesis: contradiction

then i2 - 1 < j2 - 1 by XREAL_1:11;
then i2 - 1 < j2 -' 1 by XREAL_0:def 2;
then i2 -' 1 < j2 -' 1 by A41, 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:8;
hence contradiction by A33, A37, A40, A44, A46, GOBOARD7:39; :: thesis: verum

end;

suppose j2 < i2 ; :: thesis: contradiction

then j2 - 1 < i2 - 1 by XREAL_1:11;
then j2 - 1 < i2 -' 1 by XREAL_0:def 2;
then j2 -' 1 < i2 -' 1 by A43, 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:8;
hence contradiction by A33, A37, A40, A42, A45, GOBOARD7:39; :: thesis: verum

end;

end;

end;

hence Lower_Seq (C,n) is one-to-one by FUNCT_1:def 8; :: thesis: ( Lower_Seq (C,n) is special & Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )
E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:50;
then A47: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:96, SPRECT_2:47;
hence Lower_Seq (C,n) is special by SPPOL_2:41; :: thesis: ( Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )
thus Lower_Seq (C,n) is unfolded by A47, SPPOL_2:28; :: thesis: Lower_Seq (C,n) is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis: ( j <= i + 1 or LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) )
assume A48: 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 A48, XREAL_1:237, XXREAL_0:2;
then A49: 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 A47, SPPOL_2:10;

now

per cases ( i > 0 or i = 0 ) by NAT_1:2;

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

then A50: i >= 0 + 1 by NAT_1:13;
then i = (i -' 1) + 1 by XREAL_1:237;
then A51: 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 A29, SPPOL_2:10;
(i + 1) - 1 < j - 1 by A48, XREAL_1:11;
then A52: (i - 1) + 1 < j -' 1 by XREAL_0:def 2;
i - 1 >= 0 by A50, XREAL_1:21;
then (i -' 1) + 1 < j -' 1 by A52, 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:8;
then A53: ((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))))))) ;
A54: (i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) > 0 + 1 by A28, XREAL_1:10;

now

per 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)))))) ) ;

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 A49, A51, A53, A54, GOBOARD5:def 4;
hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} by XBOOLE_0:def 7; :: thesis: verum

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 LSeg ((Lower_Seq (C,n)),j) = {} by A49, TOPREAL1:def 5;
hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; :: thesis: verum

end;

end;

end;

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

end;

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

then LSeg ((Lower_Seq (C,n)),i) = {} by TOPREAL1:def 5;
hence (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; :: thesis: verum

end;

end;

end;

hence LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) by XBOOLE_0:def 7; :: thesis: verum