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

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