theorem Th15: :: JORDAN5C:15

for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)