let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) holds B_Cut f,p,q <> {}
let p, q be Point of (TOP-REAL 2); :: thesis: B_Cut f,p,q <> {}
A1: R_Cut (L_Cut f,q),p <> {} by JORDAN1J:44;

per cases ( ( p in L~ f & q in L~ f & Index p,f < Index q,f ) or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) or ( not ( p in L~ f & q in L~ f & Index p,f < Index q,f ) & not ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) ) ;

suppose ( ( p in L~ f & q in L~ f & Index p,f < Index q,f ) or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) ; :: thesis: B_Cut f,p,q <> {}

then B_Cut f,p,q = R_Cut (L_Cut f,p),q by JORDAN3:def 8;
hence B_Cut f,p,q <> {} by JORDAN1J:44; :: thesis: verum

end;

suppose ( not ( p in L~ f & q in L~ f & Index p,f < Index q,f ) & not ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) ; :: thesis: B_Cut f,p,q <> {}

then B_Cut f,p,q = Rev (R_Cut (L_Cut f,q),p) by JORDAN3:def 8;
hence B_Cut f,p,q <> {} by A1; :: thesis: verum

end;

end;