let f be FinSequence of (TOP-REAL 2); for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
let Q be Subset of (TOP-REAL 2); for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
let q be Point of (TOP-REAL 2); ( f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) )
set P = L~ f;
assume that
A1:
f is being_S-Seq
and
A2:
(L~ f) /\ Q is closed
and
A3:
q in L~ f
and
A4:
q in Q
; LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
set q1 = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q);
A5:
(L~ f) /\ Q c= L~ f
by XBOOLE_1:17;
( L~ f meets Q & L~ f is_an_arc_of f /. 1,f /. (len f) )
by A1, A3, A4, TOPREAL1:25, XBOOLE_0:3;
then
( Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | (L~ f))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) )
by A2, A4, Def2;
hence
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
by A3, A5; verum