let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) holds
( B is_outside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not bounded Subset of (Euclid n) ) )
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_outside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not 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_outside_component_of A implies ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not bounded Subset of (Euclid n) ) ) :: thesis: ( ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not bounded Subset of (Euclid n) ) implies B is_outside_component_of A )

proof

reconsider D2 = B as Subset of (Euclid n) by TOPREAL3:8;
assume A2: B is_outside_component_of A ; :: thesis: ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not bounded Subset of (Euclid n) )
then consider C being Subset of ((TOP-REAL n) | (A `)) such that
A3: C = B and
A4: C is a_component by A1;

now :: thesis: ex D being Subset of (Euclid n) st
( D = C & not D is bounded )

assume for D being Subset of (Euclid n) st D = C holds
D is bounded ; :: thesis: contradiction
then D2 is bounded by A3;
hence contradiction by A2, Th5; :: thesis: verum

end;

hence ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is not bounded Subset of (Euclid n) ) by A3, A4; :: thesis: verum

end;

given C being Subset of ((TOP-REAL n) | (A `)) such that A5: ( C = B & C is a_component & C is not bounded Subset of (Euclid n) ) ; :: thesis: B is_outside_component_of A
( not B is bounded & B is_a_component_of A ` ) by A5, Th5, CONNSP_1:def 6;
hence B is_outside_component_of A ; :: thesis: verum