theorem :: JORDAN23:2

for f being non empty FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds len (R_Cut (f,p)) >= 1