let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st len f >= 2 & not p in L~ f holds
for n being Element of NAT st 1 <= n & n <= len f holds
f /. n <> p
let f be FinSequence of (TOP-REAL 2); :: thesis: ( len f >= 2 & not p in L~ f implies for n being Element of NAT st 1 <= n & n <= len f holds
f /. n <> p )
assume A1: ( len f >= 2 & not p in L~ f ) ; :: thesis: for n being Element of NAT st 1 <= n & n <= len f holds
f /. n <> p
given n being Element of NAT such that A2: ( 1 <= n & n <= len f & f /. n = p ) ; :: thesis: contradiction
set Mf = { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } ;

per cases ( n = len f or n < len f ) by A2, XXREAL_0:1;

suppose A3: n = len f ; :: thesis: contradiction

reconsider j = (len f) - 1 as Element of NAT by A1, INT_1:18, XXREAL_0:2;
1 + 1 <= len f by A1;
then ( 1 <= j & j + 1 <= len f ) by XREAL_1:21;
then ( f /. (j + 1) in LSeg f,j & LSeg f,j in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } ) by TOPREAL1:27;
hence contradiction by A1, A2, A3, TARSKI:def 4; :: thesis: verum

end;

suppose A4: n < len f ; :: thesis: contradiction

then n + 1 <= len f by NAT_1:13;
then A5: LSeg f,n in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A2;
( n + 1 <= len f & 1 <= n ) by A2, A4, NAT_1:13;
then f /. n in LSeg f,n by TOPREAL1:27;
hence contradiction by A1, A2, A5, TARSKI:def 4; :: thesis: verum

end;

end;