let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f & len (R_Cut f,p) >= 2 holds
f . 1 in L~ (R_Cut f,p)
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & len (R_Cut f,p) >= 2 implies f . 1 in L~ (R_Cut f,p) )
assume A1: p in L~ f ; :: thesis: ( not len (R_Cut f,p) >= 2 or f . 1 in L~ (R_Cut f,p) )
then len f <> 0 by TOPREAL1:28;
then len f > 0 by NAT_1:3;
then 0 + 1 <= len f by NAT_1:13;
then A2: (R_Cut f,p) . 1 = f . 1 by A1, JORDAN1B:4;
assume 2 <= len (R_Cut f,p) ; :: thesis: f . 1 in L~ (R_Cut f,p)
hence f . 1 in L~ (R_Cut f,p) by A2, JORDAN3:34; :: thesis: verum