let n be Element of NAT ; :: thesis: for A, B being Subset of (TOP-REAL n) st B is_a_component_of A ` holds
A misses B
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_a_component_of A ` implies A misses B )
assume B is_a_component_of A ` ; :: thesis: A misses B
then B c= A ` by SPRECT_1:5;
then A misses B by SUBSET_1:23;
hence A /\ B = {} by XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis: verum