let f be FinSequence of (); :: thesis: for Q being Subset of ()
for q being Point of ()
for i being 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 (); :: thesis: for q being Point of ()
for i being 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 (); :: thesis: for i being 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 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 that
A1: LSeg (f,i) meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: ( 1 <= i & i + 1 <= len f ) and
A5: q in LSeg (f,i) and
A6: q in Q ; :: thesis: LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
reconsider P = LSeg (f,i) as non empty Subset of () by A5;
set q1 = Last_Point (P,(f /. i),(f /. (i + 1)),Q);
set p1 = f /. i;
set p2 = f /. (i + 1);
A7: P /\ Q c= P by XBOOLE_1:17;
A8: i + 1 in dom f by ;
A9: ( f is one-to-one & i in dom f ) by ;
A10: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; :: thesis: contradiction
then i = i + 1 by ;
hence contradiction ; :: thesis: verum
end;
A11: P /\ Q is closed by ;
P is_an_arc_of f /. i,f /. (i + 1) by ;
then ( Last_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I,(() | 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, A6, A11, Def2;
then A12: LE q, Last_Point (P,(f /. i),(f /. (i + 1)),Q),P,f /. i,f /. (i + 1) by A5, A7;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by ;
hence LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) by ; :: thesis: verum