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) 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum