let i1 be Element of 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 `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = min Y holds
((GoB h) * 1,i1) `2 <= p `2
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 `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = min Y holds
((GoB h) * 1,i1) `2 <= p `2
let Y be non empty finite Subset of NAT ; :: thesis: for h being non constant standard special_circular_sequence st p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = min Y holds
((GoB h) * 1,i1) `2 <= p `2
let h be non constant standard special_circular_sequence; :: thesis: ( p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = min Y implies ((GoB h) * 1,i1) `2 <= p `2 )
assume A1: ( p `1 = W-bound (L~ h) & p in L~ h & Y = { j where j is Element of NAT : ( [1,j] in Indices (GoB h) & ex i being Element of NAT st
( i in dom h & h /. i = (GoB h) * 1,j ) ) } & i1 = min Y ) ; :: thesis: ((GoB h) * 1,i1) `2 <= p `2
then A2: p `1 = ((GoB h) * 1,1) `1 by Th39;
A3: 1 <= width (GoB h) by GOBOARD7:35;
A4: 1 <= len (GoB h) by GOBOARD7:34;
consider i being Element of NAT such that
A5: ( 1 <= i & i + 1 <= len h & p in LSeg (h /. i),(h /. (i + 1)) ) by A1, SPPOL_2:14;
i <= i + 1 by NAT_1:11;
then A6: i <= len h by A5, XXREAL_0:2;
A7: 1 <= i + 1 by A5, XREAL_1:147;

now

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

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

then LSeg (h /. i),(h /. (i + 1)) is vertical by A5, TOPREAL1:def 5;
then (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:37;
then A8: ( p `1 = (h /. (i + 1)) `1 & p `1 = (h /. i) `1 ) by A5, GOBOARD7:5;

now

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) * 1,i1) `2 <= p `2

then A9: ( (h /. i) `2 <= p `2 & p `2 <= (h /. (i + 1)) `2 ) by A5, TOPREAL1:10;
((GoB h) * 1,i1) `2 <= (h /. i) `2 by A1, A2, A4, A5, A6, A8, Th43;
hence ((GoB h) * 1,i1) `2 <= p `2 by A9, XXREAL_0:2; :: thesis: verum

end;

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

then A10: ( (h /. (i + 1)) `2 <= p `2 & p `2 <= (h /. i) `2 ) by A5, TOPREAL1:10;
((GoB h) * 1,i1) `2 <= (h /. (i + 1)) `2 by A1, A2, A4, A5, A7, A8, Th43;
hence ((GoB h) * 1,i1) `2 <= p `2 by A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

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

then LSeg (h /. i),(h /. (i + 1)) is horizontal by A5, TOPREAL1:def 5;
then (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:36;
then A11: ( p `2 = (h /. (i + 1)) `2 & p `2 = (h /. i) `2 ) by A5, GOBOARD7:6;

now

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) * 1,i1) `2 <= p `2

then A12: (h /. i) `1 <= ((GoB h) * 1,1) `1 by A2, A5, TOPREAL1:9;
(h /. i) `1 >= ((GoB h) * 1,1) `1 by A3, A5, A6, Th7;
then (h /. i) `1 = ((GoB h) * 1,1) `1 by A12, XXREAL_0:1;
hence ((GoB h) * 1,i1) `2 <= p `2 by A1, A4, A5, A6, A11, Th43; :: thesis: verum

end;

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

then A13: (h /. (i + 1)) `1 <= ((GoB h) * 1,1) `1 by A2, A5, TOPREAL1:9;
(h /. (i + 1)) `1 >= ((GoB h) * 1,1) `1 by A3, A5, A7, Th7;
then (h /. (i + 1)) `1 = ((GoB h) * 1,1) `1 by A13, XXREAL_0:1;
hence ((GoB h) * 1,i1) `2 <= p `2 by A1, A4, A5, A7, A11, Th43; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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