let n be Element of NAT ; :: thesis: for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds
B is connected
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_outside_component_of A implies B is connected )
assume B is_outside_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_of (TOP-REAL n) | (A ` ) and
C is not bounded Subset of (Euclid n) by Th18;
C is connected by A2, CONNSP_1:def 5;
hence B is connected by A1, CONNSP_1:24; :: thesis: verum