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 First_Point (L~ f),(f /. 1),(f /. (len f)),Q,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 First_Point (L~ f),(f /. 1),(f /. (len f)),Q,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 First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f) )
assume A1: ( f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q ) ; :: thesis: LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f)
then A2: L~ f meets Q by XBOOLE_0:3;
set P = L~ f;
A3: L~ f is_an_arc_of f /. 1,f /. (len f) by A1, TOPREAL1:31;
A4: (L~ f) /\ Q c= L~ f by XBOOLE_1:17;
set q1 = First_Point (L~ f),(f /. 1),(f /. (len f)),Q;
A5: First_Point (L~ f),(f /. 1),(f /. (len f)),Q in (L~ f) /\ Q by A1, A2, A3, Def1;
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 = First_Point (L~ f),(f /. 1),(f /. (len f)),Q & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds
s1 <= s2 by A1, A2, A3, Def1;
hence LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q, L~ f,f /. 1,f /. (len f) by A1, A4, A5, Def3; :: thesis: verum