let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st f is being_S-Seq & p in L~ f & q in L~ f & 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) ) ) holds

B_Cut (f,p,q) is_S-Seq_joining p,q

let p, q be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & q in L~ f & 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) ) ) implies B_Cut (f,p,q) is_S-Seq_joining p,q )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: q in L~ f and

A4: p <> q ; :: thesis: ( ( 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) ) ) or B_Cut (f,p,q) is_S-Seq_joining p,q )

assume A5: ( 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: B_Cut (f,p,q) is_S-Seq_joining p,q

then A6: B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by A2, A3, Def7;

Index (p,f) < len f by A2, Th8;

then A7: (Index (p,f)) + 1 <= len f by NAT_1:13;

A8: Index (q,f) < len f by A3, Th8;

1 <= Index (q,f) by A3, Th8;

then A9: 1 < len f by A8, XXREAL_0:2;

then A20: (L_Cut (f,p)) . 1 = p ;

then A22: Index (q,(L_Cut (f,p))) < len (L_Cut (f,p)) by Th8;

1 <= Index (q,(L_Cut (f,p))) by A21, Th8;

then 1 <= len (L_Cut (f,p)) by A22, XXREAL_0:2;

then p = (L_Cut (f,p)) /. 1 by A20, FINSEQ_4:15;

hence B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A4, A6, A10, A21, A20, Th32, Th34; :: thesis: verum

B_Cut (f,p,q) is_S-Seq_joining p,q

let p, q be Point of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & p in L~ f & q in L~ f & 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) ) ) implies B_Cut (f,p,q) is_S-Seq_joining p,q )

assume that

A1: f is being_S-Seq and

A2: p in L~ f and

A3: q in L~ f and

A4: p <> q ; :: thesis: ( ( 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) ) ) or B_Cut (f,p,q) is_S-Seq_joining p,q )

assume A5: ( 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: B_Cut (f,p,q) is_S-Seq_joining p,q

then A6: B_Cut (f,p,q) = R_Cut ((L_Cut (f,p)),q) by A2, A3, Def7;

Index (p,f) < len f by A2, Th8;

then A7: (Index (p,f)) + 1 <= len f by NAT_1:13;

A8: Index (q,f) < len f by A3, Th8;

1 <= Index (q,f) by A3, Th8;

then A9: 1 < len f by A8, XXREAL_0:2;

A10: now :: thesis: ( ( Index (p,f) < Index (q,f) & not p = f . (len f) ) or ( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) & not p = f . (len f) ) )end;

then
L_Cut (f,p) is_S-Seq_joining p,f /. (len f)
by A1, A2, Th33;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 A5;

end;

case A11:
Index (p,f) < Index (q,f)
; :: thesis: not p = f . (len f)

assume A12:
p = f . (len f)
; :: thesis: contradiction

(Index (p,f)) + 1 <= Index (q,f) by A11, NAT_1:13;

then len f <= Index (q,f) by A1, A9, A12, Th12;

hence contradiction by A3, Th8; :: thesis: verum

end;(Index (p,f)) + 1 <= Index (q,f) by A11, NAT_1:13;

then len f <= Index (q,f) by A1, A9, A12, Th12;

hence contradiction by A3, Th8; :: thesis: verum

case A13:
( Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) )
; :: thesis: not p = f . (len f)

hence contradiction by A1, A9, A14, Th12; :: thesis: verum

end;

A14: now :: thesis: not p = f . ((Index (p,f)) + 1)

assume
p = f . (len f)
; :: thesis: contradiction
q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1)))
by A13;

then consider r being Real such that

A15: q = ((1 - r) * (f /. (Index (p,f)))) + (r * (f /. ((Index (p,f)) + 1))) and

A16: 0 <= r and

A17: r <= 1 ;

A18: p = 1 * p by RLVECT_1:def 8

.= (0. (TOP-REAL 2)) + (1 * p) by RLVECT_1:4

.= ((1 - 1) * (f /. (Index (p,f)))) + (1 * p) by RLVECT_1:10 ;

assume A19: p = f . ((Index (p,f)) + 1) ; :: thesis: contradiction

then p = f /. ((Index (p,f)) + 1) by A7, FINSEQ_4:15, NAT_1:11;

then 1 <= r by A13, A15, A16, A18;

then r = 1 by A17, XXREAL_0:1;

hence contradiction by A4, A7, A19, A15, A18, FINSEQ_4:15, NAT_1:11; :: thesis: verum

end;then consider r being Real such that

A15: q = ((1 - r) * (f /. (Index (p,f)))) + (r * (f /. ((Index (p,f)) + 1))) and

A16: 0 <= r and

A17: r <= 1 ;

A18: p = 1 * p by RLVECT_1:def 8

.= (0. (TOP-REAL 2)) + (1 * p) by RLVECT_1:4

.= ((1 - 1) * (f /. (Index (p,f)))) + (1 * p) by RLVECT_1:10 ;

assume A19: p = f . ((Index (p,f)) + 1) ; :: thesis: contradiction

then p = f /. ((Index (p,f)) + 1) by A7, FINSEQ_4:15, NAT_1:11;

then 1 <= r by A13, A15, A16, A18;

then r = 1 by A17, XXREAL_0:1;

hence contradiction by A4, A7, A19, A15, A18, FINSEQ_4:15, NAT_1:11; :: thesis: verum

hence contradiction by A1, A9, A14, Th12; :: thesis: verum

then A20: (L_Cut (f,p)) . 1 = p ;

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) ) ) )end;

then A21:
q in L~ (L_Cut (f,p))
by SPPOL_2:17;( 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 A5;

end;

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) )

( 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 A2, A3, Th29;

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;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

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) )

( 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 A2, A3, A4, Th31;

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;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

then A22: Index (q,(L_Cut (f,p))) < len (L_Cut (f,p)) by Th8;

1 <= Index (q,(L_Cut (f,p))) by A21, Th8;

then 1 <= len (L_Cut (f,p)) by A22, XXREAL_0:2;

then p = (L_Cut (f,p)) /. 1 by A20, FINSEQ_4:15;

hence B_Cut (f,p,q) is_S-Seq_joining p,q by A1, A2, A4, A6, A10, A21, A20, Th32, Th34; :: thesis: verum