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 L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),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 L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

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

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

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

assume that

A1: L~ f meets Q and

A2: f is being_S-Seq and

A3: Q is closed and

A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and

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

A6: ( q in LSeg (f,i) & q in Q ) ; :: thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

len f >= 2 by A2, TOPREAL1:def 8;

then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:23;

(LSeg (f,i)) /\ Q <> {} by A6, XBOOLE_0:def 4;

then A7: LSeg (f,i) meets Q ;

Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th20;

hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm3; :: thesis: verum

for q being Point of (TOP-REAL 2)

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

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),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 L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

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

LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

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

assume that

A1: L~ f meets Q and

A2: f is being_S-Seq and

A3: Q is closed and

A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and

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

A6: ( q in LSeg (f,i) & q in Q ) ; :: thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)

len f >= 2 by A2, TOPREAL1:def 8;

then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:23;

(LSeg (f,i)) /\ Q <> {} by A6, XBOOLE_0:def 4;

then A7: LSeg (f,i) meets Q ;

Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th20;

hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm3; :: thesis: verum