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;