let n be Nat; :: thesis: 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
let R, P, Q be Subset of (TOP-REAL n); :: thesis: ( P is_outside_component_of Q & R is_inside_component_of Q implies P misses R )
assume A1: P is_outside_component_of Q ; :: thesis: ( not R is_inside_component_of Q or P misses R )
assume A2: R is_inside_component_of Q ; :: thesis: P misses R
BDD Q misses UBD Q by Th15;
then P misses BDD Q by A1, Th14, XBOOLE_1:63;
hence P misses R by A2, Th13, XBOOLE_1:63; :: thesis: verum