for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f holds
Rev g is_in_the_area_of f