let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) holds
( B is_inside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) )
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_inside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) )
A1: ( B is_a_component_of A ` iff ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component ) ) by CONNSP_1:def 6;
thus ( B is_inside_component_of A implies ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) ) by Th5, A1; :: thesis: ( ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) implies B is_inside_component_of A )
given C being Subset of ((TOP-REAL n) | (A `)) such that A2: ( C = B & C is a_component & C is bounded Subset of (Euclid n) ) ; :: thesis: B is_inside_component_of A
( B is bounded & B is_a_component_of A ` ) by A2, Th5, CONNSP_1:def 6;
hence B is_inside_component_of A ; :: thesis: verum