theorem Th80: :: JORDAN2C:96

for D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( UBD (L~ (SpStSeq D)) <> {} & UBD (L~ (SpStSeq D)) is_outside_component_of L~ (SpStSeq D) & BDD (L~ (SpStSeq D)) <> {} & BDD (L~ (SpStSeq D)) is_inside_component_of L~ (SpStSeq D) )