let i1 be Nat; for p being Point of (TOP-REAL 2)
for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
let p be Point of (TOP-REAL 2); for Y being non empty finite Subset of NAT
for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
let Y be non empty finite Subset of NAT; for h being non constant standard special_circular_sequence st p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y holds
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
let h be non constant standard special_circular_sequence; ( p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y implies ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 )
A1:
1 <= len (GoB h)
by GOBOARD7:32;
assume A2:
( p `1 = E-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [(len (GoB h)),j] in Indices (GoB h) & ex i being Nat st
( i in dom h & h /. i = (GoB h) * ((len (GoB h)),j) ) ) } & i1 = max Y )
; ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
then consider i being Nat such that
A3:
1 <= i
and
A4:
i + 1 <= len h
and
A5:
p in LSeg ((h /. i),(h /. (i + 1)))
by SPPOL_2:14;
A6:
1 <= i + 1
by A3, XREAL_1:145;
i <= i + 1
by NAT_1:11;
then A7:
i <= len h
by A4, XXREAL_0:2;
A8:
p `1 = ((GoB h) * ((len (GoB h)),1)) `1
by A2, Th39;
A9:
1 <= width (GoB h)
by GOBOARD7:33;
now ( ( LSeg (h,i) is vertical & ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ) or ( LSeg (h,i) is horizontal & ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ) )per cases
( LSeg (h,i) is vertical or LSeg (h,i) is horizontal )
by SPPOL_1:19;
case
LSeg (
h,
i) is
vertical
;
verumthen
LSeg (
(h /. i),
(h /. (i + 1))) is
vertical
by A3, A4, TOPREAL1:def 3;
then A10:
(h /. i) `1 = (h /. (i + 1)) `1
by SPPOL_1:16;
then A11:
p `1 = (h /. i) `1
by A5, GOBOARD7:5;
A12:
p `1 = (h /. (i + 1)) `1
by A5, A10, GOBOARD7:5;
per cases
( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 )
;
suppose
(h /. i) `2 >= (h /. (i + 1)) `2
;
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A13:
(h /. i) `2 >= p `2
by A5, TOPREAL1:4;
((GoB h) * ((len (GoB h)),i1)) `2 >= (h /. i) `2
by A2, A8, A1, A3, A7, A11, Th44;
hence
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
by A13, XXREAL_0:2;
verum end; suppose
(h /. i) `2 < (h /. (i + 1)) `2
;
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A14:
(h /. (i + 1)) `2 >= p `2
by A5, TOPREAL1:4;
((GoB h) * ((len (GoB h)),i1)) `2 >= (h /. (i + 1)) `2
by A2, A8, A1, A4, A6, A12, Th44;
hence
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
by A14, XXREAL_0:2;
verum end; end; end; case
LSeg (
h,
i) is
horizontal
;
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then
LSeg (
(h /. i),
(h /. (i + 1))) is
horizontal
by A3, A4, TOPREAL1:def 3;
then A15:
(h /. i) `2 = (h /. (i + 1)) `2
by SPPOL_1:15;
then A16:
p `2 = (h /. i) `2
by A5, GOBOARD7:6;
A17:
p `2 = (h /. (i + 1)) `2
by A5, A15, GOBOARD7:6;
now ( ( (h /. i) `1 >= (h /. (i + 1)) `1 & ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ) or ( (h /. i) `1 < (h /. (i + 1)) `1 & ((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 ) )per cases
( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 )
;
case
(h /. i) `1 >= (h /. (i + 1)) `1
;
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A18:
(h /. i) `1 >= ((GoB h) * ((len (GoB h)),1)) `1
by A8, A5, TOPREAL1:3;
(h /. i) `1 <= ((GoB h) * ((len (GoB h)),1)) `1
by A9, A3, A7, Th5;
then
(h /. i) `1 = ((GoB h) * ((len (GoB h)),1)) `1
by A18, XXREAL_0:1;
hence
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
by A2, A1, A3, A7, A16, Th44;
verum end; case
(h /. i) `1 < (h /. (i + 1)) `1
;
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2 then A19:
(h /. (i + 1)) `1 >= ((GoB h) * ((len (GoB h)),1)) `1
by A8, A5, TOPREAL1:3;
(h /. (i + 1)) `1 <= ((GoB h) * ((len (GoB h)),1)) `1
by A9, A4, A6, Th5;
then
(h /. (i + 1)) `1 = ((GoB h) * ((len (GoB h)),1)) `1
by A19, XXREAL_0:1;
hence
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
by A2, A1, A4, A6, A17, Th44;
verum end; end; end; hence
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
;
verum end; end; end;
hence
((GoB h) * ((len (GoB h)),i1)) `2 >= p `2
; verum