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 7;
now :: thesis: ( ( Index (p,f) < Index (q,f) & ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) & ex i1 being Nat st
( 1 <= i1 & i1 + 1 <= len (L_Cut (f,p)) & q in LSeg ((L_Cut (f,p)),i1) ) ) )
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 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:29;
hence ex i1 being 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 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:31;
hence ex i1 being 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:41, SPPOL_2:17;
L~ (L_Cut (f,p)) c= L~ f by A1, JORDAN3:42;
hence L~ (B_Cut (f,p,q)) c= L~ f by A6; :: thesis: verum