theorem Th9: :: JORDAN1B:9

for p, q being FinSequence of (TOP-REAL 2)
for v being Point of (TOP-REAL 2) st p is_in_the_area_of q holds
Rotate (p,v) is_in_the_area_of q