let f be FinSequence of (TOP-REAL 2); for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
let i be Nat; ( 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) )
assume that
A1:
( 1 <= i & i + 1 <= len f )
and
A2:
f is being_S-Seq
and
A3:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i)
; Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A3;
Q = LSeg ((f /. i),(f /. (i + 1)))
by A1, TOPREAL1:def 3;
then
Q c= L~ f
by A1, SPPOL_2:16;
then
L~ f meets Q
by A3, XBOOLE_0:3;
then A4:
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point (Q,(f /. i),(f /. (i + 1)),Q)
by A1, A2, A3, Th20;
( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) )
by A1, A2, JORDAN5B:15;
hence
Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
by A4, Th7; verum