let f be FinSequence of (TOP-REAL 2); :: thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg f,i meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1)
let Q be Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg f,i meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1)
let q be Point of (TOP-REAL 2); :: thesis: for i being Element of NAT st LSeg f,i meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q holds
LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1)
let i be Element of NAT ; :: thesis: ( LSeg f,i meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q implies LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1) )
assume A1: ( LSeg f,i meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg f,i & q in Q ) ; :: thesis: LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1)
then A2: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by TOPREAL1:def 5;
reconsider P = LSeg f,i as non empty Subset of (TOP-REAL 2) by A1;
P is closed by SPPOL_1:40;
then A3: P /\ Q is closed by A1, TOPS_1:35;
A4: P is_an_arc_of f /. i,f /. (i + 1) by A1, JORDAN5B:15;
A5: P /\ Q c= P by XBOOLE_1:17;
set q1 = Last_Point P,(f /. i),(f /. (i + 1)),Q;
set p1 = f /. i;
set p2 = f /. (i + 1);
A6: f is one-to-one by A1, TOPREAL1:def 10;
A7: ( i in dom f & i + 1 in dom f ) by A1, GOBOARD2:3;
A8: f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis: contradiction
then i = i + 1 by A6, A7, PARTFUN2:17;
hence contradiction ; :: thesis: verum

end;

A9: Last_Point P,(f /. i),(f /. (i + 1)),Q in P /\ Q by A1, A3, A4, Def2;
for g being Function of I[01] ,((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = Last_Point P,(f /. i),(f /. (i + 1)),Q & 0 <= s2 & s2 <= 1 holds
s1 <= s2 by A1, A3, A4, Def2;
then LE q, Last_Point P,(f /. i),(f /. (i + 1)),Q,P,f /. i,f /. (i + 1) by A1, A5, A9, Def3;
hence LE q, Last_Point (LSeg f,i),(f /. i),(f /. (i + 1)),Q,f /. i,f /. (i + 1) by A2, A8, Th17; :: thesis: verum