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 & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) holds
q in L~ (L_Cut (f,p))
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & p <> f . (len f) & f is being_S-Seq & not p in L~ (L_Cut (f,q)) implies q in L~ (L_Cut (f,p)) )
assume that
A1: p in L~ f and
A2: q in L~ f and
A3: p <> f . (len f) and
A4: f is being_S-Seq ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )
A5: Index (p,f) < len f by A1, JORDAN3:8;
A6: 1 <= Index (p,f) by A1, JORDAN3:8;
A7: (Index (p,f)) + 1 <= len f by A5, NAT_1:13;
then A8: LSeg (f,(Index (p,f))) = LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A6, TOPREAL1:def 3;
A9: Index (p,f) in dom f by A6, A7, SEQ_4:134;
A10: (Index (p,f)) + 1 in dom f by A6, A7, SEQ_4:134;
A11: f is one-to-one by A4;
Index (p,f) < (Index (p,f)) + 1 by NAT_1:13;
then A12: f /. (Index (p,f)) <> f /. ((Index (p,f)) + 1) by A9, A10, A11, PARTFUN2:10;

per cases ( Index (p,f) < Index (q,f) or Index (p,f) = Index (q,f) or Index (p,f) > Index (q,f) ) by XXREAL_0:1;

suppose Index (p,f) < Index (q,f) ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, JORDAN3:29; :: thesis: verum

end;

suppose A13: Index (p,f) = Index (q,f) ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

A14: p in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A1, A8, JORDAN3:9;
q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A2, A8, A13, JORDAN3:9;
then A15: ( LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) or LT q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) by A12, A14, JORDAN3:28;

now :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

per cases ( LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) or LE q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ) by A15;

suppose A16: LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

thus ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) :: thesis: verum

proof

per cases ( p <> q or p = q ) ;

suppose p <> q ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, A13, A16, JORDAN3:31; :: thesis: verum

end;

suppose p = q ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A3, A4, Th19; :: thesis: verum

end;

end;

end;

end;

suppose A17: LE q,p,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

thus ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) :: thesis: verum

proof

per cases ( p <> q or p = q ) ;

suppose p <> q ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, A13, A17, JORDAN3:31; :: thesis: verum

end;

suppose p = q ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A3, A4, Th19; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) ; :: thesis: verum

end;

suppose Index (p,f) > Index (q,f) ; :: thesis: ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) )

hence ( p in L~ (L_Cut (f,q)) or q in L~ (L_Cut (f,p)) ) by A1, A2, JORDAN3:29; :: thesis: verum

end;

end;