let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) holds len (R_Cut f,p) >= 1
let p be Point of (TOP-REAL 2); :: thesis: len (R_Cut f,p) >= 1
R_Cut f,p <> {} by JORDAN1J:44;
then len (R_Cut f,p) <> 0 ;
then ( len (R_Cut f,p) > 0 & 1 = 0 + 1 ) by NAT_1:3;
hence len (R_Cut f,p) >= 1 by NAT_1:13; :: thesis: verum