theorem :: GOBOARD2:18

for n being Nat
for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) holds
f /. n in rng (Col ((GoB f),(width (GoB f))))