theorem Th25: :: SPRECT_2:25

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