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) * 1,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) * 1,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) * 1,1) `1 ; :: 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 `1 < ((GoB f) * 1,1) `1 by A1, A3;
consider i being Element of NAT such that
A6: 1 <= i and
A7: i + 1 <= len f and
A8: x in LSeg (f /. i),(f /. (i + 1)) by A4, SPPOL_2:14;
A9: 1 < width (GoB f) by GOBOARD7:35;

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

end;

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

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

end;

end;