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_of (TOP-REAL n) | (A ` ) & 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_of (TOP-REAL n) | (A ` ) & 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_of (TOP-REAL n) | (A ` ) ) ) 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_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) ) :: thesis: ( ex C being Subset of ((TOP-REAL n) | (A ` )) st
( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & 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_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) )
then consider C being Subset of ((TOP-REAL n) | (A ` )) such that
A4: ( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) ) by A1, Def3;
B is bounded Subset of (Euclid n) by A2, A3, Def2;
hence ex C being Subset of ((TOP-REAL n) | (A ` )) st
( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) by A4; :: thesis: verum

end;

given C being Subset of ((TOP-REAL n) | (A ` )) such that A5: ( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) ; :: thesis: B is_inside_component_of A
A6: B is Bounded by A5, Def2;
B is_a_component_of A ` by A5, CONNSP_1:def 6;
hence B is_inside_component_of A by A6, Def3; :: thesis: verum