let i, j be Element of NAT ; :: thesis: for f being non constant standard special_circular_sequence st 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid f,i,j) & not i = 1 holds
j = len f
let f be non constant standard special_circular_sequence; :: thesis: ( 1 <= i & i < j & j <= len f & f /. 1 in L~ (mid f,i,j) & not i = 1 implies j = len f )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= len f ; :: thesis: ( not f /. 1 in L~ (mid f,i,j) or i = 1 or j = len f )
1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A4: f /. 1 in LSeg f,1 by TOPREAL1:27;
assume f /. 1 in L~ (mid f,i,j) ; :: thesis: ( i = 1 or j = len f )
then consider n being Element of NAT such that
A5: 1 <= n and
A6: n + 1 <= len (mid f,i,j) and
A7: f /. 1 in LSeg (mid f,i,j),n by SPPOL_2:13;
n < len (mid f,i,j) by A6, NAT_1:13;
then A8: n < (j -' i) + 1 by A1, A2, A3, JORDAN4:20;
then LSeg (mid f,i,j),n = LSeg f,((n + i) -' 1) by A1, A2, A3, A5, JORDAN4:31;
then A9: f /. 1 in (LSeg f,1) /\ (LSeg f,((n + i) -' 1)) by A7, A4, XBOOLE_0:def 4;
then A10: LSeg f,1 meets LSeg f,((n + i) -' 1) by XBOOLE_0:4;
assume that
A11: i <> 1 and
A12: j <> len f ; :: thesis: contradiction

per cases ( 1 + 1 >= (n + i) -' 1 or ((n + i) -' 1) + 1 >= len f ) by A10, GOBOARD5:def 4;

suppose 1 + 1 >= (n + i) -' 1 ; :: thesis: contradiction

then A13: n + i <= 2 + 1 by NAT_D:52;
i > 1 by A1, A11, XXREAL_0:1;
then A14: i >= 1 + 1 by NAT_1:13;
n + i >= i + 1 by A5, XREAL_1:8;
then i + 1 <= 2 + 1 by A13, XXREAL_0:2;
then i <= 2 by XREAL_1:8;
then A15: i = 2 by A14, XXREAL_0:1;
then n <= 1 by A13, XREAL_1:8;
then n = 1 by A5, XXREAL_0:1;
then A16: (n + i) -' 1 = 2 by A15, NAT_D:34;
A17: 2 < len f by GOBOARD7:36, XXREAL_0:2;
1 + 2 <= len f by GOBOARD7:36, XXREAL_0:2;
then (LSeg f,1) /\ (LSeg f,(1 + 1)) = {(f /. (1 + 1))} by TOPREAL1:def 8;
then f /. 1 = f /. 2 by A9, A16, TARSKI:def 1;
hence contradiction by A17, GOBOARD7:38; :: thesis: verum

end;

suppose A18: ((n + i) -' 1) + 1 >= len f ; :: thesis: contradiction

n <= n + i by NAT_1:11;
then A19: len f <= n + i by A5, A18, XREAL_1:237, XXREAL_0:2;
((j -' i) + 1) + i = ((j -' i) + i) + 1
.= j + 1 by A2, XREAL_1:237 ;
then n + i < j + 1 by A8, XREAL_1:8;
then A20: n + i <= j by NAT_1:13;
j < len f by A3, A12, XXREAL_0:1;
hence contradiction by A19, A20, XXREAL_0:2; :: thesis: verum

end;

end;