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