let f be FinSequence of (TOP-REAL 2); :: thesis:
let Q be Subset of (TOP-REAL 2); :: thesis:
let q be Point of (TOP-REAL 2); :: thesis:
let i be Element of NAT ; :: thesis:
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,i & q in Q ) ; :: thesis:
len f >= 2 by A2, TOPREAL1:def 10;
then reconsider P = L~ f, R = LSeg f,i as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:29;
(LSeg f,i) /\ Q <> {} by A6, XBOOLE_0:def 4;
then A7: LSeg f,i meets Q by XBOOLE_0:def 7;
Last_Point P,(f /. 1),(f /. (len f)),Q = Last_Point R,(f /. i),(f /. (i + 1)),Q by A1, A2, A3, A4, A5, Th20;
hence LE q, Last_Point (L~ f),(f /. 1),(f /. (len f)),Q,f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm3; :: thesis: