:: deftheorem defines is_inside_component_of JORDAN2C:def 2 :
for n being Nat
for A, B being Subset of (TOP-REAL n) holds
( B is_inside_component_of A iff ( B is_a_component_of A ` & B is bounded ) );