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