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:31, 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, Def3; :: thesis: verum