let f be FinSequence of ; :: thesis: for p being Point of holds R_Cut f,p <> {}
let p be Point of ; :: 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 5;
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 5;
hence R_Cut f,p <> {} ; :: thesis: verum

end;

end;