let p be Point of (); :: thesis: for f being FinSequence of () st len f >= 2 & not p in L~ f holds
for n being Nat st 1 <= n & n <= len f holds
f /. n <> p

let f be FinSequence of (); :: thesis: ( len f >= 2 & not p in L~ f implies for n being Nat st 1 <= n & n <= len f holds
f /. n <> p )

assume that
A1: len f >= 2 and
A2: not p in L~ f ; :: thesis: for n being Nat st 1 <= n & n <= len f holds
f /. n <> p

set Mf = { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } ;
given n being Nat such that A3: 1 <= n and
A4: n <= len f and
A5: f /. n = p ; :: thesis: contradiction
per cases ( n = len f or n < len f ) by ;
suppose A6: n = len f ; :: thesis: contradiction
reconsider j = (len f) - 1 as Element of NAT by ;
1 + 1 <= len f by A1;
then A7: 1 <= j by XREAL_1:19;
then A8: f /. (j + 1) in LSeg (f,j) by TOPREAL1:21;
j + 1 <= len f ;
then LSeg (f,j) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A7;
hence contradiction by A2, A5, A6, A8, TARSKI:def 4; :: thesis: verum
end;
suppose A9: n < len f ; :: thesis: contradiction
then n + 1 <= len f by NAT_1:13;
then A10: f /. n in LSeg (f,n) by ;
n + 1 <= len f by ;
then LSeg (f,n) in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A3;
hence contradiction by A2, A5, A10, TARSKI:def 4; :: thesis: verum
end;
end;