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)

for i being Nat st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

let Q be Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2)

for i being Nat st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

let q be Point of (TOP-REAL 2); :: thesis: for i being Nat st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

let i be Nat; :: thesis: ( LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) )

assume that

A1: LSeg (f,i) meets Q and

A2: f is being_S-Seq and

A3: Q is closed and

A4: ( 1 <= i & i + 1 <= len f ) and

A5: q in LSeg (f,i) and

A6: q in Q ; :: thesis: LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

reconsider P = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5;

set q1 = First_Point (P,(f /. i),(f /. (i + 1)),Q);

set p1 = f /. i;

set p2 = f /. (i + 1);

A7: P /\ Q c= P by XBOOLE_1:17;

A8: i + 1 in dom f by A4, SEQ_4:134;

A9: ( f is one-to-one & i in dom f ) by A2, A4, SEQ_4:134, TOPREAL1:def 8;

A10: f /. i <> f /. (i + 1)

P is_an_arc_of f /. i,f /. (i + 1) by A2, A4, JORDAN5B:15;

then ( First_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = First_Point (P,(f /. i),(f /. (i + 1)),Q) & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds

s1 <= s2 ) ) by A1, A6, A11, Def1;

then A12: LE First_Point (P,(f /. i),(f /. (i + 1)),Q),q,P,f /. i,f /. (i + 1) by A5, A7;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def 3;

hence LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) by A10, A12, Th17; :: thesis: verum

for q being Point of (TOP-REAL 2)

for i being Nat st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

let Q be Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2)

for i being Nat st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

let q be Point of (TOP-REAL 2); :: thesis: for i being Nat st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

let i be Nat; :: thesis: ( LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) )

assume that

A1: LSeg (f,i) meets Q and

A2: f is being_S-Seq and

A3: Q is closed and

A4: ( 1 <= i & i + 1 <= len f ) and

A5: q in LSeg (f,i) and

A6: q in Q ; :: thesis: LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)

reconsider P = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5;

set q1 = First_Point (P,(f /. i),(f /. (i + 1)),Q);

set p1 = f /. i;

set p2 = f /. (i + 1);

A7: P /\ Q c= P by XBOOLE_1:17;

A8: i + 1 in dom f by A4, SEQ_4:134;

A9: ( f is one-to-one & i in dom f ) by A2, A4, SEQ_4:134, TOPREAL1:def 8;

A10: f /. i <> f /. (i + 1)

proof

A11:
P /\ Q is closed
by A3, TOPS_1:8;
assume
f /. i = f /. (i + 1)
; :: thesis: contradiction

then i = i + 1 by A9, A8, PARTFUN2:10;

hence contradiction ; :: thesis: verum

end;then i = i + 1 by A9, A8, PARTFUN2:10;

hence contradiction ; :: thesis: verum

P is_an_arc_of f /. i,f /. (i + 1) by A2, A4, JORDAN5B:15;

then ( First_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)

for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = First_Point (P,(f /. i),(f /. (i + 1)),Q) & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds

s1 <= s2 ) ) by A1, A6, A11, Def1;

then A12: LE First_Point (P,(f /. i),(f /. (i + 1)),Q),q,P,f /. i,f /. (i + 1) by A5, A7;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def 3;

hence LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) by A10, A12, Th17; :: thesis: verum