for p being non trivial FinSequence of (TOP-REAL 2)
for v being Point of (TOP-REAL 2) holds Rotate (p,v) is_in_the_area_of p by Th9, SPRECT_2:21;