theorem :: JORDAN2C:117

for n being Nat
for A, B being Subset of (TOP-REAL n) st B is_a_component_of A ` holds
A misses B by SPRECT_1:5, SUBSET_1:23;