theorem Th1: :: JORDAN1E:1
for f, g being FinSequence of (TOP-REAL 2) st f is_in_the_area_of g holds
for p being Element of (TOP-REAL 2) st p in rng f holds
f -: p is_in_the_area_of g