let n be Element of 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;
A2: ( B is_outside_component_of A iff ( B is_a_component_of A ` & not B is Bounded ) ) by Def4;
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 A3: 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
A4: C = B and
A5: C is a_component by A1, Def4;

now

assume for D being Subset of (Euclid n) st D = C holds
D is bounded ; :: thesis: contradiction
then D2 is bounded by A4;
hence contradiction by A2, A3, Def2; :: 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 A4, A5; :: thesis: verum

end;

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