let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
len (L_Cut f,p) >= 1
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies len (L_Cut f,p) >= 1 )
assume p in L~ f ; :: thesis: len (L_Cut f,p) >= 1
then L_Cut f,p <> {} by JORDAN1E:7;
then len (L_Cut f,p) <> 0 ;
then ( len (L_Cut f,p) > 0 & 1 = 0 + 1 ) by NAT_1:3;
hence len (L_Cut f,p) >= 1 by NAT_1:13; :: thesis: verum