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 7;
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 7;
hence B_Cut (f,p,q) <> {} by A1; :: thesis: verum

end;

end;