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,1) `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,1) `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,1) `2 ; :: thesis: P misses L~ f
A2: f is_sequence_on GoB f by GOBOARD5:def 5;
assume P meets L~ f ; :: thesis: contradiction
then consider x being set such that
A3: x in P and
A4: x in L~ f by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A3;
A5: x `2 < ((GoB f) * 1,1) `2 by A1, A3;
consider j being Element of NAT such that
A6: 1 <= j and
A7: j + 1 <= len f and
A8: x in LSeg (f /. j),(f /. (j + 1)) by A4, SPPOL_2:14;
A9: 1 < len (GoB f) by GOBOARD7:34;

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 A8, TOPREAL1:10;
j <= len f by A7, NAT_1:13;
then j in dom f by A6, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A11: [i1,j1] in Indices (GoB f) and
A12: f /. j = (GoB f) * i1,j1 by A2, GOBOARD1:def 11;
A13: ( 1 <= i1 & i1 <= len (GoB f) & 1 <= j1 & j1 <= width (GoB f) ) by A11, MATRIX_1:39;
then A14: (f /. j) `2 = ((GoB f) * 1,j1) `2 by A12, GOBOARD5:2;
then 1 < j1 by A5, A10, A13, XXREAL_0:1;
then ((GoB f) * 1,1) `2 < (f /. j) `2 by A9, A13, A14, GOBOARD5:5;
hence contradiction by A1, A3, A10, XXREAL_0:2; :: thesis: verum

end;

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

then A15: (f /. (j + 1)) `2 <= x `2 by A8, TOPREAL1:10;
1 <= j + 1 by NAT_1:11;
then j + 1 in dom f by A7, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A16: [i1,j1] in Indices (GoB f) and
A17: f /. (j + 1) = (GoB f) * i1,j1 by A2, GOBOARD1:def 11;
A18: ( 1 <= i1 & i1 <= len (GoB f) & 1 <= j1 & j1 <= width (GoB f) ) by A16, MATRIX_1:39;
then A19: (f /. (j + 1)) `2 = ((GoB f) * 1,j1) `2 by A17, GOBOARD5:2;
then 1 < j1 by A5, A15, A18, XXREAL_0:1;
then ((GoB f) * 1,1) `2 < (f /. (j + 1)) `2 by A9, A18, A19, GOBOARD5:5;
hence contradiction by A1, A3, A15, XXREAL_0:2; :: thesis: verum

end;

end;