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

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