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 that
A1: len f >= 2 and
A2: not p in L~ f ; :: thesis: for n being Element of NAT st 1 <= n & n <= len f holds
f /. n <> p
set Mf = { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } ;
given n being Element of 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 A4, XXREAL_0:1;

suppose A6: 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 A7: 1 <= j by XREAL_1:21;
then A8: f /. (j + 1) in LSeg f,j by TOPREAL1:27;
j + 1 <= len f ;
then LSeg f,j in { (LSeg f,k) where k is Element of 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 A3, TOPREAL1:27;
n + 1 <= len f by A9, NAT_1:13;
then LSeg f,n in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A3;
hence contradiction by A2, A5, A10, TARSKI:def 4; :: thesis: verum

end;

end;