for n being Nat
for R, P, Q being Subset of (TOP-REAL n) st P is_outside_component_of Q & R is_inside_component_of Q holds
P misses R