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:39;
then L~ (B_Cut (f,p,q)) = {} by TOPREAL1:22;
hence L~ (B_Cut (f,p,q)) c= L~ f ; :: 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:33; :: 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: now :: thesis: ( Index (p,f) = Index (q,f) & not LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) implies LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) )

assume that
A7: Index (p,f) = Index (q,f) and
A8: 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)
A9: Index (p,f) < len f by A1, JORDAN3:8;
A10: 1 <= Index (p,f) by A1, JORDAN3:8;
then A11: Index (p,f) in dom f by A9, FINSEQ_3:25;
A12: (Index (p,f)) + 1 <= len f by A9, NAT_1:13;
then A13: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A10, TOPREAL1:def 3;
then A14: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A1, JORDAN3:9;
f . (Index (p,f)) <> f . ((Index (p,f)) + 1) by A3, A10, A9;
then A15: f /. (Index (p,f)) <> f . ((Index (p,f)) + 1) by A11, PARTFUN1:def 6;
1 <= (Index (p,f)) + 1 by NAT_1:11;
then (Index (p,f)) + 1 in dom f by A12, FINSEQ_3:25;
then A16: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A15, PARTFUN1:def 6;
q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, A7, A13, JORDAN3:9;
then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A8, A14, A16, JORDAN3:28;
hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A7, JORDAN3:def 6; :: thesis: verum

end;

A17: ( 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;
then A18: L~ (B_Cut (f,q,p)) c= L~ f by A1, A2, A4, A6, JORDAN5B:33;
B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A5, JORDAN3:def 7;
then Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A1, A2, A17, A6, JORDAN3:def 7;
hence L~ (B_Cut (f,p,q)) c= L~ f by A18, SPPOL_2:22; :: thesis: verum

end;

end;