let i1 be Nat; :: thesis: 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 `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 = min 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
for h being non constant standard special_circular_sequence 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 = min Y holds
((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
let Y be non empty finite Subset of NAT; :: thesis: for h being non constant standard special_circular_sequence 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 = min Y holds
((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
let h be non constant standard special_circular_sequence; :: 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 = min Y implies ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 )
set I = width (GoB h);
A1: 1 <= width (GoB h) by GOBOARD7:33;
assume A2: ( 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 = min Y ) ; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1
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: p `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A2, Th40;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by A4, XXREAL_0:2;
A8: 1 <= i + 1 by A3, 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 ) )

per cases ( LSeg (h,i) is horizontal or LSeg (h,i) is vertical ) by SPPOL_1:19;

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 A3, A4, TOPREAL1:def 3;
then A9: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A10: p `2 = (h /. i) `2 by A5, GOBOARD7:6;
A11: p `2 = (h /. (i + 1)) `2 by A5, A9, 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 ) )

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 ; :: thesis: ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1

then A12: (h /. i) `1 <= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,(width (GoB h)))) `1 <= (h /. i) `1 by A2, A6, A1, A3, A7, A10, Th42;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A12, XXREAL_0:2; :: thesis: verum

end;

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

then A13: (h /. (i + 1)) `1 <= p `1 by A5, TOPREAL1:3;
((GoB h) * (i1,(width (GoB h)))) `1 <= (h /. (i + 1)) `1 by A2, A6, A1, A4, A8, A11, Th42;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A13, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; :: thesis: verum

end;

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 A3, A4, TOPREAL1:def 3;
then A14: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A15: p `1 = (h /. i) `1 by A5, GOBOARD7:5;
A16: 1 <= len (GoB h) by GOBOARD7:32;
A17: p `1 = (h /. (i + 1)) `1 by A5, A14, 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 ) )

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

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

then A18: (h /. i) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A6, A5, TOPREAL1:4;
(h /. i) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A3, A7, A16, Th6;
then (h /. i) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A18, XXREAL_0:1;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A2, A1, A3, A7, A15, Th42; :: thesis: verum

end;

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

then A19: (h /. (i + 1)) `2 >= ((GoB h) * (1,(width (GoB h)))) `2 by A6, A5, TOPREAL1:4;
(h /. (i + 1)) `2 <= ((GoB h) * (1,(width (GoB h)))) `2 by A4, A8, A16, Th6;
then (h /. (i + 1)) `2 = ((GoB h) * (1,(width (GoB h)))) `2 by A19, XXREAL_0:1;
hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 by A2, A1, A4, A8, A17, Th42; :: thesis: verum

end;

end;

end;

hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; :: thesis: verum

end;

end;

end;

hence ((GoB h) * (i1,(width (GoB h)))) `1 <= p `1 ; :: thesis: verum