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 & Last_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 & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies 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, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies 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, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )

let i, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i >= j & ( i = j 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,j) and

A7: 1 <= j and

A8: j + 1 <= len f and

A9: q in Q and

A10: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; :: thesis: ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),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 = Last_Point (P,(f /. 1),(f /. (len f)),Q);

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

A11: q in L~ f by A6, SPPOL_2:17;

thus i >= j :: thesis: ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) )

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

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 & Last_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 & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies 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, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies 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, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds

( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )

let i, j 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,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i >= j & ( i = j 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,j) and

A7: 1 <= j and

A8: j + 1 <= len f and

A9: q in Q and

A10: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; :: thesis: ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),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 = Last_Point (P,(f /. 1),(f /. (len f)),Q);

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

A11: q in L~ f by A6, SPPOL_2:17;

thus i >= j :: thesis: ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) )

proof

assume
i = j
; :: thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
assume
j > i
; :: thesis: contradiction

then A12: i + 1 <= j by NAT_1:13;

j <= j + 1 by NAT_1:11;

then ( 1 <= i + 1 & j <= len f ) by A8, NAT_1:11, XXREAL_0:2;

then A13: LE f /. (i + 1),f /. j,P,f /. 1,f /. (len f) by A2, A12, Th24;

LE f /. j,q,P,f /. 1,f /. (len f) by A2, A6, A7, A8, Th25;

then A14: LE f /. (i + 1),q,P,f /. 1,f /. (len f) by A13, Th13;

(L~ f) /\ Q is closed by A3, TOPS_1:8;

then A15: LE q, Last_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A9, A11, Th16;

LE Last_Point (P,(f /. 1),(f /. (len f)),Q),f /. (i + 1),P,f /. 1,f /. (len f) by A2, A4, A5, Th26;

then LE Last_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A14, Th13;

hence contradiction by A2, A10, A15, Th12, TOPREAL1:25; :: thesis: verum

end;then A12: i + 1 <= j by NAT_1:13;

j <= j + 1 by NAT_1:11;

then ( 1 <= i + 1 & j <= len f ) by A8, NAT_1:11, XXREAL_0:2;

then A13: LE f /. (i + 1),f /. j,P,f /. 1,f /. (len f) by A2, A12, Th24;

LE f /. j,q,P,f /. 1,f /. (len f) by A2, A6, A7, A8, Th25;

then A14: LE f /. (i + 1),q,P,f /. 1,f /. (len f) by A13, Th13;

(L~ f) /\ Q is closed by A3, TOPS_1:8;

then A15: LE q, Last_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A9, A11, Th16;

LE Last_Point (P,(f /. 1),(f /. (len f)),Q),f /. (i + 1),P,f /. 1,f /. (len f) by A2, A4, A5, Th26;

then LE Last_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A14, Th13;

hence contradiction by A2, A10, A15, Th12, TOPREAL1:25; :: thesis: verum

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