set f = Rotate (Cage C,n),(W-min (L~ (Cage C,n)));
A1: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then A2: 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;
A3: len (Upper_Seq C,n) = (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by Th12;

now

let i1, j1 be set ; :: thesis: ( i1 in dom (Upper_Seq C,n) & j1 in dom (Upper_Seq C,n) & (Upper_Seq C,n) . i1 = (Upper_Seq C,n) . j1 implies not i1 <> j1 )
assume that
A4: i1 in dom (Upper_Seq C,n) and
A5: j1 in dom (Upper_Seq C,n) and
A6: (Upper_Seq C,n) . i1 = (Upper_Seq C,n) . j1 and
A7: i1 <> j1 ; :: thesis: contradiction
A8: L~ (Cage C,n) = L~ (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by REVROT_1:33;
reconsider i2 = i1, j2 = j1 as Element of NAT by A4, A5;
A9: ( i2 in Seg ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) & j2 in Seg ((E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) ) by A3, A4, A5, FINSEQ_1:def 3;
A10: (Upper_Seq C,n) . i1 = (Upper_Seq C,n) /. i2 by A4, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. i2 by A2, A9, FINSEQ_5:46 ;
A11: (Upper_Seq C,n) . j1 = (Upper_Seq C,n) /. j2 by A5, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. j2 by A2, A9, FINSEQ_5:46 ;
A12: ( 1 <= i2 & 1 <= j2 ) by A9, FINSEQ_1:3;
( j2 <= (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) & i2 <= (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ) by A9, FINSEQ_1:3;
then A13: ( j2 < len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) & i2 < len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ) by A8, SPRECT_5:17, XXREAL_0:2;

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

suppose i2 < j2 ; :: thesis: contradiction

hence contradiction by A6, A10, A11, A12, A13, GOBOARD7:38; :: thesis: verum

end;

suppose j2 < i2 ; :: thesis: contradiction

hence contradiction by A6, A10, A11, A12, A13, GOBOARD7:38; :: thesis: verum

end;

end;

end;

hence Upper_Seq C,n is one-to-one by FUNCT_1:def 8; :: thesis: ( Upper_Seq C,n is special & Upper_Seq C,n is unfolded & Upper_Seq C,n is s.n.c. )
thus Upper_Seq C,n is special ; :: thesis: ( Upper_Seq C,n is unfolded & Upper_Seq C,n is s.n.c. )
thus Upper_Seq C,n is unfolded ; :: thesis: Upper_Seq C,n is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 9 :: thesis: ( j <= i + 1 or LSeg (Upper_Seq C,n),i misses LSeg (Upper_Seq C,n),j )
assume A14: i + 1 < j ; :: thesis: LSeg (Upper_Seq C,n),i misses LSeg (Upper_Seq C,n),j
len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) > 0 by NAT_1:3;
then 0 + 1 <= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by NAT_1:13;
then A15: len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) in dom (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by FINSEQ_3:27;
A16: ( i in NAT & j in NAT ) by ORDINAL1:def 13;

now

per cases ( j + 1 <= len (Upper_Seq C,n) or j + 1 > len (Upper_Seq C,n) ) ;

suppose A17: j + 1 <= len (Upper_Seq C,n) ; :: thesis: LSeg (Upper_Seq C,n),i misses LSeg (Upper_Seq C,n),j

then A18: LSeg (Upper_Seq C,n),j = LSeg (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),j by SPPOL_2:9;
j < len (Upper_Seq C,n) by A17, NAT_1:13;
then A19: LSeg (Upper_Seq C,n),i = LSeg (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))),i by A14, SPPOL_2:9, XXREAL_0:2;
A20: j + 1 <= (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A2, A17, FINSEQ_5:45;
A21: (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 A2, FINSEQ_4:31;

now

per cases ( j + 1 < (E-max (L~ (Cage C,n))) .. (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)))) ) by A20, XXREAL_0:1;

suppose j + 1 < (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ; :: thesis: j + 1 < len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))

hence j + 1 < len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A21, XXREAL_0:2; :: thesis: verum

end;

suppose A22: j + 1 = (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ; :: thesis: not j + 1 >= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))

assume j + 1 >= len (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) ; :: thesis: contradiction
then (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 A21, A22, XXREAL_0:1;
then 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 A2, FINSEQ_4:29
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (len (Rotate (Cage C,n),(W-min (L~ (Cage C,n))))) by A15, PARTFUN1:def 8
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. 1 by FINSEQ_6:def 1
.= W-min (L~ (Cage C,n)) by A1, FINSEQ_6:98 ;
hence contradiction by TOPREAL5:25; :: thesis: verum

end;

end;

end;

hence LSeg (Upper_Seq C,n),i misses LSeg (Upper_Seq C,n),j by A14, A16, A18, A19, GOBOARD5:def 4; :: thesis: verum

end;

suppose j + 1 > len (Upper_Seq C,n) ; :: thesis: LSeg (Upper_Seq C,n),i misses LSeg (Upper_Seq C,n),j

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

end;

end;

end;

hence LSeg (Upper_Seq C,n),i misses LSeg (Upper_Seq C,n),j ; :: thesis: verum