let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg f,i )
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg f,i ) )
set X = { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
assume p in L~ f ; :: thesis: ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg f,i )
then consider Y being set such that
A1: p in Y and
A2: Y in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def 4;
ex i being Element of NAT st
( Y = LSeg f,i & 1 <= i & i + 1 <= len f ) by A2;
hence ex i being Element of NAT st
( 1 <= i & i + 1 <= len f & p in LSeg f,i ) by A1; :: thesis: verum