theorem Th43: :: JORDAN5D:43

for h being non constant standard special_circular_sequence
for I, i1, i being Nat
for Y being non empty finite Subset of NAT st 1 <= i & i <= len h & 1 <= I & I <= width (GoB h) & Y = { j where j is Element of NAT : ( [j,I] in Indices (GoB h) & ex k being Nat st
( k in dom h & h /. k = (GoB h) * (j,I) ) ) } & (h /. i) `2 = ((GoB h) * (1,I)) `2 & i1 = max Y holds
((GoB h) * (i1,I)) `1 >= (h /. i) `1