for f being non trivial FinSequence of (TOP-REAL 2) holds <*(SW-corner (L~ f))*> is_in_the_area_of f