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 being_S-Seq 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 being_S-Seq 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 being_S-Seq ; :: thesis: L~ (B_Cut (f,p,q)) c= L~ f
A4: f is one-to-one by A3;

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, A4, Th21;
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, Lm3; :: thesis: verum

end;

suppose that A5: p <> q and
A6: ( 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

A7: B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A6, JORDAN3:def 7;
A8: ( 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 A6, XXREAL_0:1;

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

end;

then A20: Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A1, A2, A7, A8, JORDAN3:def 7;
L~ (B_Cut (f,q,p)) c= L~ f by A1, A2, A5, A8, A9, Lm3;
hence L~ (B_Cut (f,p,q)) c= L~ f by A20, SPPOL_2:22; :: thesis: verum

end;

end;