let f be non constant standard special_circular_sequence; :: thesis: for P being Subset of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) holds
P misses L~ f
let P be Subset of (TOP-REAL 2); :: thesis: ( ( for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ) implies P misses L~ f )
assume A1: for p being Point of (TOP-REAL 2) st p in P holds
p `2 > ((GoB f) * (1,(width (GoB f)))) `2 ; :: thesis: P misses L~ f
assume P meets L~ f ; :: thesis: contradiction
then consider x being object such that
A2: x in P and
A3: x in L~ f by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A2;
A4: x `2 > ((GoB f) * (1,(width (GoB f)))) `2 by A1, A2;
A5: 1 < len (GoB f) by GOBOARD7:32;
A6: f is_sequence_on GoB f by GOBOARD5:def 5;
consider j being Nat such that
A7: 1 <= j and
A8: j + 1 <= len f and
A9: x in LSeg ((f /. j),(f /. (j + 1))) by A3, SPPOL_2:14;

per cases ( (f /. j) `2 >= (f /. (j + 1)) `2 or (f /. j) `2 <= (f /. (j + 1)) `2 ) ;

suppose (f /. j) `2 >= (f /. (j + 1)) `2 ; :: thesis: contradiction

then A10: (f /. j) `2 >= x `2 by A9, TOPREAL1:4;
j <= len f by A8, NAT_1:13;
then j in dom f by A7, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. j = (GoB f) * (i1,j1) by A6, GOBOARD1:def 9;
A13: 1 <= j1 by A11, MATRIX_0:32;
A14: j1 <= width (GoB f) by A11, MATRIX_0:32;
( 1 <= i1 & i1 <= len (GoB f) ) by A11, MATRIX_0:32;
then A15: (f /. j) `2 = ((GoB f) * (1,j1)) `2 by A12, A13, A14, GOBOARD5:1;
then j1 < width (GoB f) by A4, A10, A14, XXREAL_0:1;
then ((GoB f) * (1,(width (GoB f)))) `2 > (f /. j) `2 by A5, A13, A15, GOBOARD5:4;
hence contradiction by A1, A2, A10, XXREAL_0:2; :: thesis: verum

end;

suppose (f /. j) `2 <= (f /. (j + 1)) `2 ; :: thesis: contradiction

then A16: (f /. (j + 1)) `2 >= x `2 by A9, TOPREAL1:4;
1 <= j + 1 by NAT_1:11;
then j + 1 in dom f by A8, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A17: [i1,j1] in Indices (GoB f) and
A18: f /. (j + 1) = (GoB f) * (i1,j1) by A6, GOBOARD1:def 9;
A19: 1 <= j1 by A17, MATRIX_0:32;
A20: j1 <= width (GoB f) by A17, MATRIX_0:32;
( 1 <= i1 & i1 <= len (GoB f) ) by A17, MATRIX_0:32;
then A21: (f /. (j + 1)) `2 = ((GoB f) * (1,j1)) `2 by A18, A19, A20, GOBOARD5:1;
then j1 < width (GoB f) by A4, A16, A20, XXREAL_0:1;
then ((GoB f) * (1,(width (GoB f)))) `2 > (f /. (j + 1)) `2 by A5, A19, A21, GOBOARD5:4;
hence contradiction by A1, A2, A16, XXREAL_0:2; :: thesis: verum

end;

end;