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 )
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
A4: ( 1 <= n & n + 1 <= len (mid f,i,j) ) and
A5: f /. 1 in LSeg (mid f,i,j),n by SPPOL_2:13;
assume that
A6: i <> 1 and
A7: j <> len f ; :: thesis: contradiction
n < len (mid f,i,j) by A4, NAT_1:13;
then A8: n < (j -' i) + 1 by A1, A2, A3, JORDAN4:20;
then A9: LSeg (mid f,i,j),n = LSeg f,((n + i) -' 1) by A1, A2, A3, A4, JORDAN4:31;
1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then f /. 1 in LSeg f,1 by TOPREAL1:27;
then A10: f /. 1 in (LSeg f,1) /\ (LSeg f,((n + i) -' 1)) by A5, A9, XBOOLE_0:def 4;
then A11: LSeg f,1 meets LSeg f,((n + i) -' 1) by XBOOLE_0:4;

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

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

then A12: n + i <= 2 + 1 by NAT_D:52;
n + i >= i + 1 by A4, XREAL_1:8;
then i + 1 <= 2 + 1 by A12, XXREAL_0:2;
then A13: i <= 2 by XREAL_1:8;
i > 1 by A1, A6, XXREAL_0:1;
then i >= 1 + 1 by NAT_1:13;
then A14: i = 2 by A13, XXREAL_0:1;
then n <= 1 by A12, XREAL_1:8;
then n = 1 by A4, XXREAL_0:1;
then A15: (n + i) -' 1 = 2 by A14, NAT_D:34;
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 A16: f /. 1 = f /. 2 by A10, A15, TARSKI:def 1;
2 < len f by GOBOARD7:36, XXREAL_0:2;
hence contradiction by A16, GOBOARD7:38; :: thesis: verum

end;

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

n <= n + i by NAT_1:11;
then A18: len f <= n + i by A4, A17, XREAL_1:237, XXREAL_0:2;
A19: j < len f by A3, A7, XXREAL_0:1;
((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 n + i <= j by NAT_1:13;
hence contradiction by A18, A19, XXREAL_0:2; :: thesis: verum

end;

end;