let i1 be Nat; :: thesis: for p being Point of ()
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 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 (); :: 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 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 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 Nat st
( i in dom h & h /. i = (GoB h) * (1,j) ) )
}
& i1 = min Y implies ((GoB h) * (1,i1)) `2 <= p `2 )

A1: 1 <= len (GoB h) by GOBOARD7:32;
assume A2: ( 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 Nat st
( i in dom h & h /. i = (GoB h) * (1,j) ) )
}
& i1 = min Y ) ; :: thesis: ((GoB h) * (1,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 ;
i <= i + 1 by NAT_1:11;
then A7: i <= len h by ;
A8: p `1 = ((GoB h) * (1,1)) `1 by ;
A9: 1 <= width (GoB h) by GOBOARD7:33;
now :: thesis: ( ( LSeg (h,i) is vertical & ((GoB h) * (1,i1)) `2 <= p `2 ) or ( LSeg (h,i) is horizontal & ((GoB h) * (1,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 ; :: thesis: ((GoB h) * (1,i1)) `2 <= p `2
then LSeg ((h /. i),(h /. (i + 1))) is vertical by ;
then A10: (h /. i) `1 = (h /. (i + 1)) `1 by SPPOL_1:16;
then A11: p `1 = (h /. i) `1 by ;
A12: p `1 = (h /. (i + 1)) `1 by ;
now :: thesis: ( ( (h /. i) `2 <= (h /. (i + 1)) `2 & ((GoB h) * (1,i1)) `2 <= p `2 ) or ( (h /. i) `2 > (h /. (i + 1)) `2 & ((GoB h) * (1,i1)) `2 <= p `2 ) )
per cases ) `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 A13: (h /. i) `2 <= p `2 by ;
((GoB h) * (1,i1)) `2 <= (h /. i) `2 by A2, A8, A1, A3, A7, A11, Th41;
hence ((GoB h) * (1,i1)) `2 <= p `2 by ; :: thesis: verum
end;
case (h /. i) `2 > (h /. (i + 1)) `2 ; :: thesis: ((GoB h) * (1,i1)) `2 <= p `2
then A14: (h /. (i + 1)) `2 <= p `2 by ;
((GoB h) * (1,i1)) `2 <= (h /. (i + 1)) `2 by A2, A8, A1, A4, A6, A12, Th41;
hence ((GoB h) * (1,i1)) `2 <= p `2 by ; :: 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 ;
then A15: (h /. i) `2 = (h /. (i + 1)) `2 by SPPOL_1:15;
then A16: p `2 = (h /. i) `2 by ;
A17: p `2 = (h /. (i + 1)) `2 by ;
now :: thesis: ( ( (h /. i) `1 <= (h /. (i + 1)) `1 & ((GoB h) * (1,i1)) `2 <= p `2 ) or ( (h /. i) `1 > (h /. (i + 1)) `1 & ((GoB h) * (1,i1)) `2 <= p `2 ) )
per cases ) `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 A18: (h /. i) `1 <= ((GoB h) * (1,1)) `1 by ;
(h /. i) `1 >= ((GoB h) * (1,1)) `1 by A9, A3, A7, Th5;
then (h /. i) `1 = ((GoB h) * (1,1)) `1 by ;
hence ((GoB h) * (1,i1)) `2 <= p `2 by A2, A1, A3, A7, A16, Th41; :: thesis: verum
end;
case (h /. i) `1 > (h /. (i + 1)) `1 ; :: thesis: ((GoB h) * (1,i1)) `2 <= p `2
then A19: (h /. (i + 1)) `1 <= ((GoB h) * (1,1)) `1 by ;
(h /. (i + 1)) `1 >= ((GoB h) * (1,1)) `1 by A9, A4, A6, Th5;
then (h /. (i + 1)) `1 = ((GoB h) * (1,1)) `1 by ;
hence ((GoB h) * (1,i1)) `2 <= p `2 by A2, A1, A4, A6, A17, Th41; :: 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