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 `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) 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 `1 > ((GoB f) * ((len (GoB f)),1)) `1 ) implies P misses L~ f )
assume A1: for p being Point of (TOP-REAL 2) st p in P holds
p `1 > ((GoB f) * ((len (GoB f)),1)) `1 ; :: 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 `1 > ((GoB f) * ((len (GoB f)),1)) `1 by A1, A2;
A5: 1 < width (GoB f) by GOBOARD7:33;
A6: f is_sequence_on GoB f by GOBOARD5:def 5;
consider i being Nat such that
A7: 1 <= i and
A8: i + 1 <= len f and
A9: x in LSeg ((f /. i),(f /. (i + 1))) by A3, SPPOL_2:14;

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

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

then A10: (f /. i) `1 >= x `1 by A9, TOPREAL1:3;
i <= len f by A8, NAT_1:13;
then i 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 /. i = (GoB f) * (i1,j1) by A6, GOBOARD1:def 9;
A13: 1 <= i1 by A11, MATRIX_0:32;
A14: i1 <= len (GoB f) by A11, MATRIX_0:32;
( 1 <= j1 & j1 <= width (GoB f) ) by A11, MATRIX_0:32;
then A15: (f /. i) `1 = ((GoB f) * (i1,1)) `1 by A12, A13, A14, GOBOARD5:2;
then i1 < len (GoB f) by A4, A10, A14, XXREAL_0:1;
then ((GoB f) * ((len (GoB f)),1)) `1 > (f /. i) `1 by A5, A13, A15, GOBOARD5:3;
hence contradiction by A1, A2, A10, XXREAL_0:2; :: thesis: verum

end;

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

then A16: (f /. (i + 1)) `1 >= x `1 by A9, TOPREAL1:3;
1 <= i + 1 by NAT_1:11;
then i + 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 /. (i + 1) = (GoB f) * (i1,j1) by A6, GOBOARD1:def 9;
A19: 1 <= i1 by A17, MATRIX_0:32;
A20: i1 <= len (GoB f) by A17, MATRIX_0:32;
( 1 <= j1 & j1 <= width (GoB f) ) by A17, MATRIX_0:32;
then A21: (f /. (i + 1)) `1 = ((GoB f) * (i1,1)) `1 by A18, A19, A20, GOBOARD5:2;
then i1 < len (GoB f) by A4, A16, A20, XXREAL_0:1;
then ((GoB f) * ((len (GoB f)),1)) `1 > (f /. (i + 1)) `1 by A5, A19, A21, GOBOARD5:3;
hence contradiction by A1, A2, A16, XXREAL_0:2; :: thesis: verum

end;

end;