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, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies 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); :: thesis: for q being Point of (TOP-REAL 2)
for i, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies 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); :: thesis: for i, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
let i, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i <= j & ( i = j 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 and
A6: i + 1 <= len f and
A7: q in LSeg (f,j) and
A8: ( 1 <= j & j + 1 <= len f ) and
A9: q in Q and
A10: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; :: thesis: ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A4, SPPOL_2:17;
set q1 = First_Point (P,(f /. 1),(f /. (len f)),Q);
set p1 = f /. i;
A11: q in L~ f by A7, SPPOL_2:17;
thus i <= j :: thesis: ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) )

proof

(L~ f) /\ Q is closed by A3, TOPS_1:8;
then A12: LE First_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A2, A9, A11, Th15;
A13: LE q,f /. (j + 1),P,f /. 1,f /. (len f) by A2, A7, A8, Th26;
i <= i + 1 by NAT_1:11;
then A14: i <= len f by A6, XXREAL_0:2;
assume j < i ; :: thesis: contradiction
then A15: j + 1 <= i by NAT_1:13;
1 <= j + 1 by NAT_1:11;
then LE f /. (j + 1),f /. i,P,f /. 1,f /. (len f) by A2, A15, A14, Th24;
then A16: LE q,f /. i,P,f /. 1,f /. (len f) by A13, Th13;
LE f /. i, First_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A4, A5, A6, Th25;
then LE q, First_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A16, Th13;
hence contradiction by A2, A10, A12, Th12, TOPREAL1:25; :: thesis: verum

end;

assume i = j ; :: thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) by A1, A2, A3, A4, A5, A6, A7, A9, Lm2; :: thesis: verum