let f be non constant standard special_circular_sequence; 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); ( ( 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
; P misses L~ f
assume
P meets L~ f
; 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) * (1,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
;
contradictionthen 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
1
< i1
by A4, A10, A13, XXREAL_0:1;
then
((GoB f) * (1,1)) `1 < (f /. i) `1
by A5, A14, A15, GOBOARD5:3;
hence
contradiction
by A1, A2, A10, XXREAL_0:2;
verum end; suppose
(f /. i) `1 >= (f /. (i + 1)) `1
;
contradictionthen 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
1
< i1
by A4, A16, A19, XXREAL_0:1;
then
((GoB f) * (1,1)) `1 < (f /. (i + 1)) `1
by A5, A20, A21, GOBOARD5:3;
hence
contradiction
by A1, A2, A16, XXREAL_0:2;
verum end; end;