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 & f is weakly-one-to-one 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 & f is weakly-one-to-one 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: f is weakly-one-to-one ; :: thesis: L~ (B_Cut f,p,q) c= L~ f

per cases ( p = q or ( p <> q & ( 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 ( p <> q & not 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 = q ; :: thesis: L~ (B_Cut f,p,q) c= L~ f

then B_Cut f,p,q = <*p*> by A1, A3, Th15;
then len (B_Cut f,p,q) = 1 by FINSEQ_1:56;
then L~ (B_Cut f,p,q) = {} by TOPREAL1:28;
hence L~ (B_Cut f,p,q) c= L~ f by XBOOLE_1:2; :: thesis: verum

end;

suppose ( p <> q & ( 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: L~ (B_Cut f,p,q) c= L~ f

hence L~ (B_Cut f,p,q) c= L~ f by A1, A2, JORDAN5B:36; :: thesis: verum

end;

suppose that A4: p <> q and
A5: ( not 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: L~ (B_Cut f,p,q) c= L~ f

A6: B_Cut f,p,q = Rev (R_Cut (L_Cut f,q),p) by A5, JORDAN3:def 8;
A7: ( Index q,f < Index p,f or ( Index p,f = Index q,f & not LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) by A5, XXREAL_0:1;

A8: now

assume that
A9: Index p,f = Index q,f and
A10: not LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ; :: thesis: LE q,p,f /. (Index q,f),f /. ((Index q,f) + 1)
A11: 1 <= Index p,f by A1, JORDAN3:41;
A12: Index p,f < len f by A1, JORDAN3:41;
then A13: (Index p,f) + 1 <= len f by NAT_1:13;
then A14: LSeg f,(Index p,f) = LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A11, TOPREAL1:def 5;
then A15: p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A1, JORDAN3:42;
A16: q in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1)) by A2, A9, A14, JORDAN3:42;
A17: Index p,f in dom f by A11, A12, FINSEQ_3:27;
1 <= (Index p,f) + 1 by NAT_1:11;
then A18: (Index p,f) + 1 in dom f by A13, FINSEQ_3:27;
f . (Index p,f) <> f . ((Index p,f) + 1) by A3, A11, A12, Def2;
then f /. (Index p,f) <> f . ((Index p,f) + 1) by A17, PARTFUN1:def 8;
then f /. (Index p,f) <> f /. ((Index p,f) + 1) by A18, PARTFUN1:def 8;
then LT q,p,f /. (Index p,f),f /. ((Index p,f) + 1) by A10, A15, A16, JORDAN3:63;
hence LE q,p,f /. (Index q,f),f /. ((Index q,f) + 1) by A9, JORDAN3:def 7; :: thesis: verum

end;

then A19: Rev (B_Cut f,q,p) = B_Cut f,p,q by A1, A2, A6, A7, JORDAN3:def 8;
L~ (B_Cut f,q,p) c= L~ f by A1, A2, A4, A7, A8, JORDAN5B:36;
hence L~ (B_Cut f,p,q) c= L~ f by A19, SPPOL_2:22; :: thesis: verum

end;

end;