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:3;
then A1: len (L_Cut (f,p)) > 0 by NAT_1:3;
1 = 0 + 1 ;
hence len (L_Cut (f,p)) >= 1 by A1, NAT_1:13; :: thesis: verum