let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st B is_inside_component_of A holds
B is connected
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_inside_component_of A implies B is connected )
assume B is_inside_component_of A ; :: thesis: B is connected
then consider C being Subset of ((TOP-REAL n) | (A `)) such that
A1: C = B and
A2: C is a_component and
C is bounded Subset of (Euclid n) by Th7;
C is connected by A2, CONNSP_1:def 5;
hence B is connected by A1, CONNSP_1:23; :: thesis: verum