theorem Th8: :: JORDAN2C:14

for n being Nat
for A, B being Subset of (TOP-REAL n) holds
( B is_outside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not bounded Subset of (Euclid n) ) )