let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st 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) ) ) & p <> q holds
L~ (B_Cut f,p,q) c= L~ f
let p, q be Point of (TOP-REAL 2); :: thesis: ( 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) ) ) & p <> q implies L~ (B_Cut f,p,q) c= L~ f )
assume that
A1: p in L~ f and
A2: q in L~ f and
A3: ( 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) ) ) and
A4: p <> q ; :: thesis: L~ (B_Cut f,p,q) c= L~ f
A5: B_Cut f,p,q = R_Cut (L_Cut f,p),q by A1, A2, A3, JORDAN3:def 8;

now

per cases ( 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) ) ) by A3;

case Index p,f < Index q,f ; :: thesis: ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 )

then q in L~ (L_Cut f,p) by A1, A2, JORDAN3:64;
hence ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 ) by SPPOL_2:13; :: thesis: verum

end;

case ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ; :: thesis: ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 )

then q in L~ (L_Cut f,p) by A1, A2, A4, JORDAN3:66;
hence ex i1 being Element of NAT st
( 1 <= i1 & i1 + 1 <= len (L_Cut f,p) & q in LSeg (L_Cut f,p),i1 ) by SPPOL_2:13; :: thesis: verum

end;

end;

end;

then A6: L~ (B_Cut f,p,q) c= L~ (L_Cut f,p) by A5, JORDAN3:76, SPPOL_2:17;
L~ (L_Cut f,p) c= L~ f by A1, JORDAN3:77;
hence L~ (B_Cut f,p,q) c= L~ f by A6, XBOOLE_1:1; :: thesis: verum