let h be non constant standard special_circular_sequence; :: thesis: for i1 being Nat

for p being Point of (TOP-REAL 2)

for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds

((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

let i1 be Nat; :: thesis: for p being Point of (TOP-REAL 2)

for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds

((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

let p be Point of (TOP-REAL 2); :: thesis: for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds

((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

let Y be non empty finite Subset of NAT; :: thesis: ( p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y implies ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 )

assume A1: ( p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y ) ; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

then consider i being Nat such that

A2: 1 <= i and

A3: i + 1 <= len h and

A4: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;

A5: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A1, Th40;

i <= i + 1 by NAT_1:11;

then A6: i <= len h by A3, XXREAL_0:2;

A7: 1 <= i + 1 by A2, XREAL_1:145;

for p being Point of (TOP-REAL 2)

for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds

((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

let i1 be Nat; :: thesis: for p being Point of (TOP-REAL 2)

for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds

((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

let p be Point of (TOP-REAL 2); :: thesis: for Y being non empty finite Subset of NAT st p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y holds

((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

let Y be non empty finite Subset of NAT; :: thesis: ( p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y implies ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 )

assume A1: ( p `2 = N-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [j,(width (GoB h))] in Indices (GoB h) & ex i being Nat st

( i in dom h & h /. i = (GoB h) * (j,(width (GoB h))) ) ) } & i1 = max Y ) ; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

then consider i being Nat such that

A2: 1 <= i and

A3: i + 1 <= len h and

A4: p in LSeg ((h /. i),(h /. (i + 1))) by SPPOL_2:14;

A5: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A1, Th40;

i <= i + 1 by NAT_1:11;

then A6: i <= len h by A3, XXREAL_0:2;

A7: 1 <= i + 1 by A2, XREAL_1:145;

now :: thesis: ( ( LSeg (h,i) is horizontal & ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) or ( LSeg (h,i) is vertical & ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) )end;

hence
((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
; :: thesis: verumper cases
( LSeg (h,i) is horizontal or LSeg (h,i) is vertical )
by SPPOL_1:19;

end;

case
LSeg (h,i) is horizontal
; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

then
LSeg ((h /. i),(h /. (i + 1))) is horizontal
by A2, A3, TOPREAL1:def 3;

then A8: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;

then A9: p `2 = (h /. i) `2 by A4, GOBOARD7:6;

A10: p `2 = (h /. (i + 1)) `2 by A4, A8, GOBOARD7:6;

end;then A8: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;

then A9: p `2 = (h /. i) `2 by A4, GOBOARD7:6;

A10: p `2 = (h /. (i + 1)) `2 by A4, A8, GOBOARD7:6;

now :: thesis: ( ( (h /. i) `1 >= (h /. (i + 1)) `1 & ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) or ( (h /. i) `1 < (h /. (i + 1)) `1 & ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) )end;

hence
((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
; :: thesis: verumper cases
( (h /. i) `1 >= (h /. (i + 1)) `1 or (h /. i) `1 < (h /. (i + 1)) `1 )
;

end;

case A11:
(h /. i) `1 >= (h /. (i + 1)) `1
; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

1 <= width (GoB h)
by GOBOARD7:33;

then A12: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. i) `1 by A1, A5, A2, A6, A9, Th43;

(h /. i) `1 >= p `1 by A4, A11, TOPREAL1:3;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A12, XXREAL_0:2; :: thesis: verum

end;then A12: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. i) `1 by A1, A5, A2, A6, A9, Th43;

(h /. i) `1 >= p `1 by A4, A11, TOPREAL1:3;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A12, XXREAL_0:2; :: thesis: verum

case A13:
(h /. i) `1 < (h /. (i + 1)) `1
; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

1 <= width (GoB h)
by GOBOARD7:33;

then A14: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. (i + 1)) `1 by A1, A5, A3, A7, A10, Th43;

(h /. (i + 1)) `1 >= p `1 by A4, A13, TOPREAL1:3;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A14, XXREAL_0:2; :: thesis: verum

end;then A14: ((GoB h) * (i1,(width (GoB h)))) `1 >= (h /. (i + 1)) `1 by A1, A5, A3, A7, A10, Th43;

(h /. (i + 1)) `1 >= p `1 by A4, A13, TOPREAL1:3;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A14, XXREAL_0:2; :: thesis: verum

case
LSeg (h,i) is vertical
; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

then
LSeg ((h /. i),(h /. (i + 1))) is vertical
by A2, A3, TOPREAL1:def 3;

then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;

then A16: p `1 = (h /. i) `1 by A4, GOBOARD7:5;

A17: 1 <= len (GoB h) by GOBOARD7:32;

A18: p `1 = (h /. (i + 1)) `1 by A4, A15, GOBOARD7:5;

end;then A15: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;

then A16: p `1 = (h /. i) `1 by A4, GOBOARD7:5;

A17: 1 <= len (GoB h) by GOBOARD7:32;

A18: p `1 = (h /. (i + 1)) `1 by A4, A15, GOBOARD7:5;

now :: thesis: ( ( (h /. i) `2 >= (h /. (i + 1)) `2 & ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) or ( (h /. i) `2 < (h /. (i + 1)) `2 & ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 ) )end;

hence
((GoB h) * (i1,(width (GoB h)))) `1 >= p `1
; :: thesis: verumper cases
( (h /. i) `2 >= (h /. (i + 1)) `2 or (h /. i) `2 < (h /. (i + 1)) `2 )
;

end;

case
(h /. i) `2 >= (h /. (i + 1)) `2
; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

then A19:
(h /. i) `2 >= ((GoB h) * (1,(width (GoB h)))) `2
by A5, A4, TOPREAL1:4;

(h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A2, A6, A17, Th6;

then A20: (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1;

1 <= width (GoB h) by GOBOARD7:33;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A2, A6, A16, A20, Th43; :: thesis: verum

end;(h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A2, A6, A17, Th6;

then A20: (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1;

1 <= width (GoB h) by GOBOARD7:33;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A2, A6, A16, A20, Th43; :: thesis: verum

case
(h /. i) `2 < (h /. (i + 1)) `2
; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1

then A21:
(h /. (i + 1)) `2 >= ((GoB h) * (1,(width (GoB h)))) `2
by A5, A4, TOPREAL1:4;

(h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A17, Th6;

then A22: (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A21, XXREAL_0:1;

1 <= width (GoB h) by GOBOARD7:33;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A3, A7, A18, A22, Th43; :: thesis: verum

end;(h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A17, Th6;

then A22: (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A21, XXREAL_0:1;

1 <= width (GoB h) by GOBOARD7:33;

hence ((GoB h) * (i1,(width (GoB h)))) `1 >= p `1 by A1, A3, A7, A18, A22, Th43; :: thesis: verum