let n be Nat; :: thesis:
let P, P1 be Subset of (TOP-REAL n); :: thesis:
let Q be Subset of (TOP-REAL n); :: thesis:
let W be Subset of (Euclid n); :: thesis:
assume that
A1: P = W and
A2: P is connected and
A3: not W is bounded and
A4: P1 = Component_of (Down (P,(Q `))) and
A5: W misses Q ; :: thesis:
A6: (TOP-REAL n) | P is connected by A2, CONNSP_1:def 3;
A7: Down (P,(Q `)) = P \ Q by SUBSET_1:13
.= P by A1, A5, XBOOLE_1:83 ;
then reconsider P0 = P as Subset of ((TOP-REAL n) | (Q `)) ;
reconsider W0 = Component_of P0 as Subset of (Euclid n) by A4, A7, TOPREAL3:8;
P0 c= Q ` by A1, A5, SUBSET_1:23;
then ((TOP-REAL n) | (Q `)) | P0 = (TOP-REAL n) | P by PRE_TOPC:7;
then A8: P0 is connected by A6, CONNSP_1:def 3;

A9: now :: thesis:

assume for D being Subset of (Euclid n) st D = P1 holds
D is bounded ; :: thesis:
then W0 is bounded by A4, A7;
hence contradiction by A1, A3, A8, CONNSP_3:1, TBSP_1:14; :: thesis:

end;

A10: W <> {} (Euclid n) by A3;
A11: W /\ Q = {} by A5;

assume Q ` = {} ; :: thesis:
then Q = ({} the carrier of (TOP-REAL n)) ` ;
hence contradiction by A1, A10, A11, XBOOLE_1:28; :: thesis:

end;

then reconsider Q1 = Q ` as non empty Subset of (TOP-REAL n) ;
not (TOP-REAL n) | Q1 is empty ;
then Component_of P0 is a_component by A1, A10, A8, CONNSP_3:9;
hence P1 is_outside_component_of Q by A4, A7, A9, Th8; :: thesis: