let f be FinSequence of (TOP-REAL 2); 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 & 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 (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 & 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 (TOP-REAL 2); 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; ( 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 )
; LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),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
;
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; verum