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 Element of 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 Element of 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 Element of 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 Element of 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 A1:
( 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 )
; :: thesis: ( i >= j & ( i = j implies LE q, Last_Point (L~ f),(f /. 1),(f /. (len f)),Q,f /. i,f /. (i + 1) ) )
then A2:
q in L~ f
by SPPOL_2:17;
reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A1, SPPOL_2:17;
set q1 = Last_Point P,(f /. 1),(f /. (len f)),Q;
set p2 = f /. (i + 1);
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
j > i
;
:: thesis: contradiction
then A3:
i + 1
<= j
by NAT_1:13;
(
i <= i + 1 &
j <= j + 1 )
by NAT_1:11;
then
( 1
<= i + 1 &
j <= len f )
by A1, XXREAL_0:2;
then A4:
LE f /. (i + 1),
f /. j,
P,
f /. 1,
f /. (len f)
by A1, A3, Th24;
LE f /. j,
q,
P,
f /. 1,
f /. (len f)
by A1, Th25;
then A5:
LE f /. (i + 1),
q,
P,
f /. 1,
f /. (len f)
by A4, Th13;
LE Last_Point P,
(f /. 1),
(f /. (len f)),
Q,
f /. (i + 1),
P,
f /. 1,
f /. (len f)
by A1, Th26;
then A6:
LE Last_Point P,
(f /. 1),
(f /. (len f)),
Q,
q,
P,
f /. 1,
f /. (len f)
by A5, Th13;
L~ f is
closed
by SPPOL_1:49;
then A7:
(
L~ f meets Q &
(L~ f) /\ Q is
closed &
P is_an_arc_of f /. 1,
f /. (len f) )
by A1, TOPREAL1:31, TOPS_1:35;
then
LE q,
Last_Point P,
(f /. 1),
(f /. (len f)),
Q,
P,
f /. 1,
f /. (len f)
by A1, A2, Th16;
hence
contradiction
by A1, A6, A7, Th12;
:: thesis: verum
end;
assume
i = j
; :: thesis: 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, Lm5; :: thesis: verum