theorem :: GOBOARD2:15

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
(X_axis f) . n <= (X_axis f) . m ) holds
f /. n in rng (Line ((GoB f),1))