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

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

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) ) or ( 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) ) ) )
;

end;

suppose
( 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

end;

end;

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

B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A5, Def7;

then A18: Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A2, A3, A17, A6, Def7;

B_Cut (f,q,p) is_S-Seq_joining q,p by A1, A2, A3, A4, A17, A6, Lm1;

hence B_Cut (f,p,q) is_S-Seq_joining p,q by A18, Th15; :: thesis: verum

end;

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

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;A7:
Index (p,f) < len f
by A2, Th8;

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

1 <= (Index (p,f)) + 1 by NAT_1:11;

then A9: (Index (p,f)) + 1 in dom f by A8, FINSEQ_3:25;

A10: (Index (p,f)) + 0 <> (Index (p,f)) + 1 ;

A11: 1 <= Index (p,f) by A2, Th8;

then A12: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A8, TOPREAL1:def 3;

then A13: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, Th9;

Index (p,f) in dom f by A11, A7, FINSEQ_3:25;

then A14: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A1, A9, A10, PARTFUN2:10;

assume that

A15: Index (p,f) = Index (q,f) and

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

q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A15, A12, Th9;

then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A16, A13, A14, Th28;

hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A15; :: thesis: verum

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

1 <= (Index (p,f)) + 1 by NAT_1:11;

then A9: (Index (p,f)) + 1 in dom f by A8, FINSEQ_3:25;

A10: (Index (p,f)) + 0 <> (Index (p,f)) + 1 ;

A11: 1 <= Index (p,f) by A2, Th8;

then A12: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A8, TOPREAL1:def 3;

then A13: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, Th9;

Index (p,f) in dom f by A11, A7, FINSEQ_3:25;

then A14: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A1, A9, A10, PARTFUN2:10;

assume that

A15: Index (p,f) = Index (q,f) and

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

q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A3, A15, A12, Th9;

then LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) by A16, A13, A14, Th28;

hence LE q,p,f /. (Index (q,f)),f /. ((Index (q,f)) + 1) by A15; :: thesis: verum

B_Cut (f,p,q) = Rev (R_Cut ((L_Cut (f,q)),p)) by A5, Def7;

then A18: Rev (B_Cut (f,q,p)) = B_Cut (f,p,q) by A2, A3, A17, A6, Def7;

B_Cut (f,q,p) is_S-Seq_joining q,p by A1, A2, A3, A4, A17, A6, Lm1;

hence B_Cut (f,p,q) is_S-Seq_joining p,q by A18, Th15; :: thesis: verum