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 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 Nat st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) )
set X = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
assume p in L~ f ; :: thesis: ex i being 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 Nat : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def 4;
ex i being Nat st
( Y = LSeg (f,i) & 1 <= i & i + 1 <= len f ) by A2;
hence ex i being Nat st
( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) by A1; :: thesis: verum