theorem Th48: :: JORDAN2C:63

for n being Nat
for P, P1, Q being Subset of (TOP-REAL n)
for W being Subset of (Euclid n) st P = W & P is connected & not W is bounded & P1 = Component_of (Down (P,(Q `))) & W misses Q holds
P1 is_outside_component_of Q