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
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,1)) `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;