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 being Element of 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); :: thesis: for q being Point of (TOP-REAL 2)
for i being Element of 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); :: thesis: for i being Element of 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 Element of 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 A1: ( 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 ) ; :: thesis: LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q,f /. i,f /. (i + 1)
then (LSeg f,i) /\ Q <> {} by XBOOLE_0:def 4;
then A2: LSeg f,i meets Q by XBOOLE_0:def 7;
len f >= 2 by A1, TOPREAL1:def 10;
then reconsider P = L~ f, R = LSeg f,i as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:29;
First_Point P,(f /. 1),(f /. (len f)),Q = First_Point R,(f /. i),(f /. (i + 1)),Q by A1, Th19;
hence LE First_Point (L~ f),(f /. 1),(f /. (len f)),Q,q,f /. i,f /. (i + 1) by A1, A2, Lm2; :: thesis: verum