let n be Element of 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;
A2: ( B is_inside_component_of A iff ( B is_a_component_of A ` & B is Bounded ) ) by Def3;
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) ) ) :: 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 )

proof

assume A3: B is_inside_component_of A ; :: thesis: ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) )
then B is bounded Subset of (Euclid n) by A2, Def2;
hence ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) by A1, A3, Def3; :: thesis: verum

end;

given C being Subset of ((TOP-REAL n) | (A `)) such that A4: ( 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 A4, Def2, CONNSP_1:def 6;
hence B is_inside_component_of A by Def3; :: thesis: verum