let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) holds R_Cut (f,p) <> {}
let p be Point of (TOP-REAL 2); :: thesis: R_Cut (f,p) <> {}

per cases ( p <> f . 1 or p = f . 1 ) ;

suppose p <> f . 1 ; :: thesis: R_Cut (f,p) <> {}

then R_Cut (f,p) = (mid (f,1,(Index (p,f)))) ^ <*p*> by JORDAN3:def 4;
hence R_Cut (f,p) <> {} ; :: thesis: verum

end;

suppose p = f . 1 ; :: thesis: R_Cut (f,p) <> {}

then R_Cut (f,p) = <*p*> by JORDAN3:def 4;
hence R_Cut (f,p) <> {} ; :: thesis: verum

end;

end;