let f be FinSequence of (); :: thesis: for Q being Subset of ()
for q being Point of ()
for i being Nat st L~ f meets Q & f is being_S-Seq & Q is closed & First_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 First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)

let Q be Subset of (); :: thesis: for q being Point of ()
for i being Nat st L~ f meets Q & f is being_S-Seq & Q is closed & First_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 First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)

let q be Point of (); :: thesis: for i being Nat st L~ f meets Q & f is being_S-Seq & Q is closed & First_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 First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)

let i be Nat; :: thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & First_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 First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),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: First_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 First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
len f >= 2 by ;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of () by ;
(LSeg (f,i)) /\ Q <> {} by ;
then A7: LSeg (f,i) meets Q ;
First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th19;
hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm1; :: thesis: verum